Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:2201.11221 · Mathematical Structures in Computer Science

A linear linear lambda-calculus

Alejandro Díaz-Caro, Gilles Dowek B

Published May 31, 2024• 6 citations
arXivHTMLPDF

Abstract

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.

DOI
10.1017/s0960129524000197

Related papers

Linear Lambda-Calculus is Linear

Alejandro Díaz-Caro, Gilles Dowek B

We prove a linearity theorem for an extension of linear logic with addition and multiplication by a scalar: the proofs of some propositions in this logic are linear in the algebraic sense. This work is part of a wider research program that aims at defining a logic whose proof language is a quantum programming language.

Leibniz international proceedings in informatics•Jan 1, 2022•0 citations

Linear-algebraic lambda-calculus

Pablo J. Arrighi, Gilles Dowek B

With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite system. The linear-algebraic lambda-calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear lambda-calculus. These various notions of linearity are discussed in the context of quantum programming languages. KEYWORDS: quantum lambda-calculus, linear lambda-calculus, $λ$-calculus, quantum logics.

arXiv:quant-ph/0501150•Jan 25, 2005•7 citations

An algebraic extension of intuitionistic linear logic: the 𝓛!𝒮-calculus and its categorical model

Alejandro Díaz-Caro, Malena Ivnisky, Octavio Malherbe

Abstract We introduce the ${{\mathcal L}_!^{\mathcal S}}$-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic. These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the ${{\mathcal L}_{!}^{\mathcal S}}$-calculus as an extension of the ${\mathcal L}^{\mathcal S}$-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalization and an introduction property—as well as preserve the expressiveness of the original ${\mathcal L}^{\mathcal S}$-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.

arXiv:2504.12128•Journal of Logic and Computation•Nov 4, 2025•0 citations

Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams

Bert Lindenhovius, Michael W. Mislove, Vladimir Zamdzhiev

Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus for string diagrams, introduced by Rios and Selinger (with primary application in quantum computing). Our abstract treatment of this language leads to simpler concrete models compared to those presented so far. We also extend the language with general recursion and prove soundness. Finally, we present an adequacy result for the diagram-free fragment of the language which corresponds to a modified version of Benton and Wadler's adjoint calculus with recursion.

arXiv:1804.09822•Apr 25, 2018•2 citations

Linear-algebraic Lambda-calculus: higher-order, encodings and confluence

Pablo J. Arrighi, Gilles Dowek B

We introduce a minimal language combining both higher-order computation and linear algebra. Roughly, this is nothing else than the Lambda-calculus together with the possibility to make linear combinations of terms a.t+b.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in field of quantum computation, which we show can be easily encoded in the calculus, as well as in other domains such as the interpretation of linear logic. Finally we prove the confluence of the calculus, this is our main result. Keywords: quantum programming language, quantum control, quantum logic, probabilistic and quantitative analysis, rewriting techniques.

•Dec 22, 2006•30 citations

Operational semantics for formal tensorial calculus

Pablo J. Arrighi, Gilles Dowek B

With a view towards models of quantum computation, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite systems. The linear-algebraic -calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear -calculus. These various notions of linearity are discussed in the context of quantum programming languages .

•Jan 1, 2004•16 citations
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.
With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite system. The linear-algebraic lambda-calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear lambda-calculus. These various notions of linearity are discussed in the context of quantum programming languages. KEYWORDS: quantum lambda-calculus, linear lambda-calculus, λλλ-calculus, quantum logics.
Abstract We introduce the L!S{{\mathcal L}_!^{\mathcal S}}L!S​-calculus, a linear lambda-calculus extended with scalar multiplication and term addition, that acts as a proof language for intuitionistic linear logic. These algebraic operations enable the direct expression of linearity at the syntactic level, a property not typically available in standard proof-term calculi. Building upon previous work, we develop the L!S{{\mathcal L}_{!}^{\mathcal S}}L!S​-calculus as an extension of the LS{\mathcal L}^{\mathcal S}LS-calculus with the ! modality. We prove key meta-theoretical properties—subject reduction, confluence, strong normalization and an introduction property—as well as preserve the expressiveness of the original LS{\mathcal L}^{\mathcal S}LS-calculus, including the encoding of vectors and matrices, and the correspondence between proof-terms and linear functions. A denotational semantics is provided in the framework of linear categories with biproducts, ensuring a sound and adequate interpretation of the calculus. This work is part of a broader programme aiming to build a measurement-free quantum programming language grounded in linear logic.
Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus for string diagrams, introduced by Rios and Selinger (with primary application in quantum computing). Our abstract treatment of this language leads to simpler concrete models compared to those presented so far. We also extend the language with general recursion and prove soundness. Finally, we present an adequacy result for the diagram-free fragment of the language which corresponds to a modified version of Benton and Wadler's adjoint calculus with recursion.
We introduce a minimal language combining both higher-order computation and linear algebra. Roughly, this is nothing else than the Lambda-calculus together with the possibility to make linear combinations of terms a.t+b.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in field of quantum computation, which we show can be easily encoded in the calculus, as well as in other domains such as the interpretation of linear logic. Finally we prove the confluence of the calculus, this is our main result. Keywords: quantum programming language, quantum control, quantum logic, probabilistic and quantitative analysis, rewriting techniques.
With a view towards models of quantum computation, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite systems. The linear-algebraic -calculus hereby constructed is linear in a different (yet related) sense to that, say, of the linear -calculus. These various notions of linearity are discussed in the context of quantum programming languages .