A mad day’s work in theoretical computer science, mathematical logic, algebraic geometry and statistical learning theory.
The seminar takes place on every second Thursday (see below for the schedule) at 11am-12pm Melbourne time. If we’re not in lockdown the venue will be the Russell Love room of Peter Hall at the University of Melbourne. The seminars will be streamed live via Zoom unless advertised otherwise in the schedule below, and questions can be directed to the speaker, via a moderator, via Zoom chat. In between seminars discussions and announcements take place on the Rising Sea Discord. Talks will be recorded and posted to the CGL YouTube channel within about a week.
Co-organised by Will Troiani and Daniel Murfet.
Schedule
- 6-5 Will Troiani - Proof-nets - notes, video
- 3-6 Will Troiani - Proof-nets: the Sequentialisation Theorem - notes, video
- 17-6 Will Troiani - Geometry of Interaction zero: proofs as permutations - notes, video.
- 8-7 Tom Waring - System F: strong normalisation - notes.
- 22-7 Daniel Murfet - Matrix factorisations - in metauni locus LC001. For the mathematical content see video1, video2, video3 and for questions see this.
Upcoming:
- Daniel Murfet - The cut operation on matrix factorisations
- James Clift - Smooth relaxations of Turing machines
- Will Troiani - Geometry of Interaction I: proofs as operators
Abstracts
Will Troiani “Proof-nets: the sequentialisation theorem”
Proof-structures, invented by J.Y.Girard in his 1986 paper “Linear Logic”, are a variant on sequent style proofs. Proof-structures are non-sequential in nature so the translation of sequent style linear logic proofs into proof-nets erases information about the order of connectives. The map from sequent calculus proofs to proof-structures is not surjective, and the image of this translation are the proof-nets. This leads to the question: how can we intrinsically characterise proof-nets among proof-structures?
The answer to this question is given by the Sequentialization Theorem, which gives a correctness criterion which detects proof-nets among proof-structures. This correctness criterion is the foundation upon which Girard’s Geometry of Interaction I, a program set on interpreting proof-nets geometrically, rests. This two part talk is dedicated to proving the Sequentialization Theorem. The first part will be concerned with carefully defining sequent style linear logic, proof-nets, and the translation from one to the other. The second part will then proceed to the proof of the Theorem.
Technical
Zoom is running on the iMac in Russell Love, with a video feed (Extron MediaPort 2000) from the in-room camera at the back of the room, and an audio feed from the same camera. The speaker is wearing both a lapel mic connected to in-room speakers (primarily so that their voice is audible to the camera’s microphone, which is not amazing) and a second mic which feeds audio to an app on an iPhone in their pocket (for the YouTube recording). The moderator is signed into the Zoom meeting and the Discord channel to monitor for questions.