Quantum Computation, Categorical Semantics and Linear Logic
Andre van Tonder and Miquel Dorca
Discussion led by Xiang Long on April 13, 2015
Abstract:
PDFWe develop a type theory and provide a denotational semantics for a simple fragment of the quantum lambda calculus, a formal language for quantum computation based on linear logic. In our semantics, terms inhabit certain Hilbert bundles, and computations are interpreted as the appropriate inner product preserving maps between Hilbert bundles. These bundles and maps form a symmetric monoidal closed category, as expected for a calculus based on linear logic.