IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation

TL;DR

This paper presents a logical framework for quantum computation that integrates mixed states and measurement within a proof language, enabling formal reasoning about quantum processes.

Contribution

It introduces a novel proof language for IMALL extended with a modality B, capturing mixed-state quantum computation and measurement as definable terms.

Findings

Represented any linear map on C2 within the system

Demonstrated the system's expressiveness with quantum teleportation

Ensured soundness of cut-elimination with respect to denotational semantics

Abstract

We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality B to capture mixed-state quantum computation. The language supports algebraic constructs such as linear combinations, and embeds pure quantum computations within a mixed-state framework via B, interpreted categorically as a functor from a category of Hilbert Spaces to a category of finite-dimensional C*-algebras. Measurement arises as a definable term, not as a constant, and the system avoids the use of quantum configurations, which are part of the theory of the quantum lambda calculus. Cut-elimination is defined via a composite reduction relation, and shown to be sound with respect to the denotational interpretation. We prove n that any linear map on C 2 can be represented within the system, and illustrate this expressiveness with examples such as quantum teleportation and the quantum switch.