A Geometrical Logic for Information Flow

I will describe a new kind of 2-dimensional 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 finite-state 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!