Mathematical methods for resource-based type theories

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 (37)

• Quantifying Coherence
• Quantum Coherence as a Resource
• Quantum Resource Theories
• Operational Resource Theory of Coherence
• Fundamental limitations for quantum and nano thermodynamics
• Description of quantum coherence in thermodynamic processes requires constraints beyond free energy
• The second laws of quantum thermodynamics
• The Resource Theory of Quantum States Out of Thermal Equilibrium
• Informational derivation of Quantum Theory
• On the quantum, classical and total amount of correlations in a quantum state
• Robustness of coherence: An operational and observable measure of quantum coherence
• The Resource Theory of Stabilizer Computation
• 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
• The general structure of quantum resource theories
• How to quantify coherence: Distinguishing speakable and unspeakable notions
• Low-temperature thermodynamics with quantum coherence
• A mathematical theory of resources
• Relating the Resource Theories of Entanglement and Quantum Coherence
• Concrete Categorical Model of a Quantum Circuit Description Language with Measurement
• Reversible transformations from pure to mixed states, and the unique measure of information
• A Resource Framework for Quantum Shannon Theory
• Maximal Coherence and the Resource Theory of Purity
• The Minimal Work Cost of Information Processing
• Quantifying Contextuality
• Structure of the resource theory of quantum coherence
• Quantum resource theories in the single-shot regime
• The asymmetry properties of pure quantum states
• Quantification and manipulation of magic states
• Noncontextual wirings
• Axiomatic approach to contextuality and nonlocality
• Oracles and query lower bounds in generalised probabilistic theories
• Symmetrizing Cost of Quantum States
• Simulating Symmetric Time Evolution With Local Operations
• Parallel Self-Testing of the GHZ State with a Proof by Diagrams
• Operational Theories of Physics as Categories