01529nas a2200109 4500008004100000245005800041210005700099520118800156100002101344700001701365856003701382 2018 eng d00aMathematical methods for resource-based type theories0 aMathematical methods for resourcebased type theories3 a
With the wide range of quantum programming languages on offer now, efficient program verification and type checking for these languages presents a challenge -- especially when classical debugging techniques may affect the states in a quantum program. In this work, we make progress towards a program verification approach using the formalism of operational quantum mechanics and resource theories. We present a logical framework that captures two mathematical approaches to resource theory based on monoids (algebraic) and monoidal categories (categorical). We develop the syntax of this framework as an intuitionistic sequent calculus, and prove soundness and completeness of an algebraic and categorical semantics that recover these approaches. We also provide a cut-elimination theorem, normal form, and analogue of Lambek's lifting theorem for polynomial systems over the logics. Using these approaches along with the Curry-Howard-Lambek correspondence for programs, proofs and categories, this work lays the mathematical groundwork for a type checker for some resource theory based frameworks, with the possibility of extending it other quantum programming languages.
1 aSundaram, Aarthi1 aLackey, Brad uhttps://arxiv.org/abs/1812.08726