A linear linear lambda-calculus

Abstract

We present a linearity theorem for a proof language of intuitionistic multiplicative additive linear logic, incorporating addition and scalar multiplication. The proofs in this language are linear in the algebraic sense. This work is part of a broader research program aiming to define a logic with a proof language that forms a quantum programming language.

This is the full revised journal version of the FSCD 2022 paper published at LIPIcs 228:21, 2022

References in corpus (2)

• A New Connective in Natural Deduction, and its Application to Quantum Computing
• The Sup Connective in IMALL: A Categorical Semantics

Cited by in corpus (6)

• 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
• A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
• 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