Mathematical methods for resource-based type theories

TL;DR

This paper develops a formal logical framework combining algebraic and categorical methods to support resource-based type theories in quantum programming, aiding program verification.

Contribution

It introduces a novel intuitionistic sequent calculus for resource theories, with soundness, completeness, and cut-elimination proofs, laying groundwork for quantum program type checkers.

Findings

Logical framework captures algebraic and categorical resource theories

Proves soundness, completeness, and cut-elimination for the framework

Provides a foundation for resource theory-based quantum program verification

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.