A Geometric Logic for Classical and Quantum Computation

Jamie Vicary

I will describe a new kind of 2-dimensional type theory, with a geometrical syntax built from points, lines and surfaces. This allow computational tasks, such as encryption and decryption, to be represented as equations between topological structures, with a classical semantics giving back the standard notion of one-time-pad encrypted communication. Under an alternative quantum semantics, the same syntax gives rise to quantum teleportation, giving a strong new mathematical connection between classical and quantum computing.

Everything will be presented in a straightforward way, with lots of pictures. No knowledge of quantum computing is necessary to understand this talk!