A linear proof language for second-order intuitionistic linear logic

Abstract

We present a polymorphic linear lambda-calculus as a proof language for second-order intuitionistic linear logic. The calculus includes addition and scalar multiplication, enabling the proof of a linearity result at the syntactic level.

arXiv commentarXiv admin note: substantial text overlap with arXiv:2201.11221

References in corpus (8)

• A functional quantum programming language
• The Vectorial $\lambda$-Calculus
• Two linearities for quantum computing in the lambda calculus
• Linearity in the non-deterministic call-by-value setting
• Realizability in the Unitary Sphere
• A New Connective in Natural Deduction, and its Application to Quantum Computing
• A System F accounting for scalars
• A linear linear lambda-calculus

Cited by in corpus (2)

• Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
• An Algebraic Extension of Intuitionistic Linear Logic: The $L_{!}^S$-Calculus and Its Categorical Model