Mathematical methods for resource-based type theories
arXiv:1812.08726
Abstract
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.
41 pages
References in corpus (6)
- Description of quantum coherence in thermodynamic processes requires constraints beyond free energy
- On the quantum, classical and total amount of correlations in a quantum state
- Quantum coherence, time-translation symmetry and thermodynamics
- The resource theory of quantum reference frames: manipulations and monotones
- Application of a resource theory for magic states to fault-tolerant quantum computing
- Simulating Symmetric Time Evolution With Local Operations