A New Connective in Natural Deduction, and its Application to Quantum Computing

Abstract

We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue that these connectives model the information-erasure, the non-reversibility, and the non-determinism that occur, among other places, in quantum measurement. We introduce an intuitionistic propositional logic with a non-harmonious logical connective sup and two interstitial rules, and show that the proof language of this logic forms the core of a quantum programming language.

Accepted at TCS

References in corpus (3)

• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
• Propositional superposition logic
• Semantics for first-order superposition logic

Cited by in corpus (6)

• A linear linear lambda-calculus
• The Sup Connective in IMALL: A Categorical Semantics
• Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
• A linear proof language for second-order intuitionistic linear logic
• IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
• An Algebraic Extension of Intuitionistic Linear Logic: The $L_{!}^S$-Calculus and Its Categorical Model