A linear linear lambda-calculus
Alejandro D\'iaz-Caro, Gilles Dowek
TL;DR
This paper proves a linearity theorem for a proof language based on intuitionistic linear logic, incorporating algebraic operations, as part of developing a quantum programming language.
Contribution
It introduces a linearity theorem for a proof language with algebraic features, advancing the foundation for a quantum programming logic.
Findings
Proofs are linear in the algebraic sense.
The language incorporates addition and scalar multiplication.
Supports the development of quantum programming languages.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Mechanics and Applications · Logic, programming, and type systems · Quantum Computing Algorithms and Architecture