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:1804.09822

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

Bert Lindenhovius, Michael W. Mislove, Vladimir Zamdzhiev

Published Apr 25, 2018• 2 citations
arXivHTMLPDF

Abstract

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.

DOI
10.48550/arxiv.1804.09822

Related papers

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

On a Fully Abstract Model for a Quantum Linear Functional Language

Peter Selinger, Benoît Valiron

This paper studies the linear fragment of the programing language for quantum computation with classical control described in [Selinger, P. and B. Valiron, A lambda calculus for quantum computation with classical control, in: P. Urzyczyn, editor, Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), Lecture Notes in Computer Science 3461 (2005), pp. 354–368]. We sketch the language, and discuss equivalence of terms. We also describe a fully abstract denotational semantics based on completely positive maps.

Electronic Notes in Theoretical Computer Science•Jul 1, 2008•45 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

A linear linear lambda-calculus

Alejandro Díaz-Caro, Gilles Dowek B

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.

arXiv:2201.11221•Mathematical Structures in Computer Science•May 31, 2024•6 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

A functional programming language for quantum computation with classical control

Benoît Valiron

The objective of this thesis is to develop a functional programming language for quantum computers based on the QRAM model, following the work of P. Selinger (2004) on quantum flow-charts. We construct a lambda-calculus without side-effects to deal with quantum bits. We equip this calculus with a probabilistic call-by-value operational semantics. Since quantum information cannot be duplicated due to the no-cloning property, we need a resource-sensitive type system. We develop it based on affine intuitionistic linear logic. Unlike the quantum lambda-calculus proposed by Van Tonder (2003, 2004), the resulting lambda-calculus has only one lambda-abstraction, linear and non-linear abstractions being encoded in the type system. We also integrate classical and quantum data types within our language. The main results of this work are the subject-reduction of the language and the construction of a type inference algorithm.

•Jan 1, 2004•17 citations
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.
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.
This paper studies the linear fragment of the programing language for quantum computation with classical control described in [Selinger, P. and B. Valiron, A lambda calculus for quantum computation with classical control, in: P. Urzyczyn, editor, Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), Lecture Notes in Computer Science 3461 (2005), pp. 354–368]. We sketch the language, and discuss equivalence of terms. We also describe a fully abstract denotational semantics based on completely positive maps.
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.
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.
The objective of this thesis is to develop a functional programming language for quantum computers based on the QRAM model, following the work of P. Selinger (2004) on quantum flow-charts. We construct a lambda-calculus without side-effects to deal with quantum bits. We equip this calculus with a probabilistic call-by-value operational semantics. Since quantum information cannot be duplicated due to the no-cloning property, we need a resource-sensitive type system. We develop it based on affine intuitionistic linear logic. Unlike the quantum lambda-calculus proposed by Van Tonder (2003, 2004), the resulting lambda-calculus has only one lambda-abstraction, linear and non-linear abstractions being encoded in the type system. We also integrate classical and quantum data types within our language. The main results of this work are the subject-reduction of the language and the construction of a type inference algorithm.