A Geometrical Logic for Information Flow
Jamie Vicary ( University of Oxford )

16:30 22nd October 2013 ( week 2, Michaelmas Term 2013 )Lecture Theatre B
I will describe a new kind of 2dimensional type theory, with an unusual geometrical syntax built from points, lines
and surfaces. The resulting diagrams form readable descriptions of informatic tasks, and equations between diagrams
give specifications for interesting procedures such as encrypted communication or secret sharing. Security properties
can also be represented geometrically, and have fully geometrical proofs. A relational semantics gives the correct interpretation
of these procedures in terms of finitestate machines. With an alternative quantum semantics, the encrypted communication specification
yields exactly quantum teleportation, giving a hint of a deep structural congruence between classical and quantum computation, and
even insights into unsolved questions in the foundations of quantum physics.
Everything will be described from the beginning, with lots of pictures, and should make sense to a general audience!