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:2504.12128 · Journal of Logic and Computation

An algebraic extension of intuitionistic linear logic: the đť“›!đť’®-calculus and its categorical model

Alejandro DĂ­az-Caro, Malena Ivnisky, Octavio Malherbe

Published Nov 4, 2025• 0 citations
arXivHTMLPDF

Abstract

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.

DOI
10.1093/logcom/exaf053

Related papers

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

A Linear Sup-Calculus for Quantum Measurement

France École Normale Supérieure Paris-Saclay, Gilles Dowek B

Non-harmonious logical connectives have recently been shown to provide a natural proof-theoretic account of quantum measurement. In particular, the connective \(\mathbin{\mathsf{sup}}\) introduced by DĂ­az-Caro and Dowek endows intuitionistic natural deduction with both harmonious and excessive rules, and its proof language forms the core of a quantum programming language. However, the resulting calculus is still permissive enough to express non-linear or genuinely non-physical operations: nothing in the type system enforces linearity or prevents the cloning of quantum data. In this paper we introduce a linear version of the \(\mathbin{\mathsf{sup}}\)-calculus. We separate classical and quantum data by means of a two-zone context discipline, and we restrict the use of the \(\mathbin{\mathsf{sup}}\)-connective and scalar combinations to ensure that well-typed quantum programs denote linear maps between finite-dimensional Hilbert spaces. We give a natural deduction style type system, an operational semantics with both deterministic and measurement steps, and we prove subject reduction and type soundness. We then show that no term in the purely quantum fragment can implement a duplicator \(\mathsf{qbit} \multimap \mathsf{qbit} \otimes \mathsf{qbit}\), while classical outcomes of measurements can still be duplicated freely. Finally, we sketch a denotational semantics in which closed quantum terms denote completely positive maps, and we relate our system to existing quantum \(\lambda\)-calculi.

Bulletin of Computer and Data Sciences•Dec 30, 2024•0 citations

A concrete model for a typed linear algebraic lambda calculus

Alejandro DĂ­az-Caro, Octavio Malherbe

Abstract We give an adequate, concrete, categorical-based model for Lambda- ${\mathcal S}$ , which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda- ${\mathcal S}$ is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda- ${\mathcal S}$ has a superposition constructor S such that a type A is considered as the base of a vector space, while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over $\mathbb C$ . The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

arXiv:1806.09236•Mathematical Structures in Computer Science•Nov 21, 2023•4 citations

A concrete categorical semantics of Lambda-S

Alejandro DĂ­az-Caro, Octavio Malherbe

Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S have a constructor S such that a type A is considered as the base of a vector space while S(A) is its span. A first semantics of this calculus have been given when first presented, with such an interpretation: superposed types are interpreted as vectors spaces while non-superposed types as their basis. In this paper we give a concrete categorical semantics of Lambda-S, showing that S is interpreted as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.

•Jun 24, 2018•2 citations

A Concrete Categorical Semantics of Lambda- S

Alejandro DĂ­az-Caro, Octavio Malherbe

Lambda- S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda- S have a constructor S such that a type A is considered as the base of a vector space while S ( A ) is its span. A first semantics of this calculus have been given when first presented, with such an interpretation: superposed types are interpreted as vectors spaces while non-superposed types as their basis. In this paper we give a concrete categorical semantics of Lambda- S , showing that S is interpreted as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C . The right adjoint is a forgetful functor U , which is hidden in the language, and plays a central role in the computational reasoning.

Electronic Notes in Theoretical Computer Science•Aug 1, 2019•6 citations
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.
Non-harmonious logical connectives have recently been shown to provide a natural proof-theoretic account of quantum measurement. In particular, the connective sup\mathbin{\mathsf{sup}}sup introduced by Díaz-Caro and Dowek endows intuitionistic natural deduction with both harmonious and excessive rules, and its proof language forms the core of a quantum programming language. However, the resulting calculus is still permissive enough to express non-linear or genuinely non-physical operations: nothing in the type system enforces linearity or prevents the cloning of quantum data. In this paper we introduce a linear version of the sup\mathbin{\mathsf{sup}}sup-calculus. We separate classical and quantum data by means of a two-zone context discipline, and we restrict the use of the sup\mathbin{\mathsf{sup}}sup-connective and scalar combinations to ensure that well-typed quantum programs denote linear maps between finite-dimensional Hilbert spaces. We give a natural deduction style type system, an operational semantics with both deterministic and measurement steps, and we prove subject reduction and type soundness. We then show that no term in the purely quantum fragment can implement a duplicator qbit⊸qbit⊗qbit\mathsf{qbit} \multimap \mathsf{qbit} \otimes \mathsf{qbit}qbit⊸qbit⊗qbit, while classical outcomes of measurements can still be duplicated freely. Finally, we sketch a denotational semantics in which closed quantum terms denote completely positive maps, and we relate our system to existing quantum λ\lambdaλ-calculi.
Abstract We give an adequate, concrete, categorical-based model for Lambda- S{\mathcal S}S , which is a typed version of a linear-algebraic lambda calculus, extended with measurements. Lambda- S{\mathcal S}S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi: to forbid duplication of variables and to consider all lambda-terms as algebraic linear functions. The type system of Lambda- S{\mathcal S}S has a superposition constructor S such that a type A is considered as the base of a vector space, while SA is its span. Our model considers S as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C\mathbb CC . The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.
Lambda-S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda-S have a constructor S such that a type A is considered as the base of a vector space while S(A) is its span. A first semantics of this calculus have been given when first presented, with such an interpretation: superposed types are interpreted as vectors spaces while non-superposed types as their basis. In this paper we give a concrete categorical semantics of Lambda-S, showing that S is interpreted as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C. The right adjoint is a forgetful functor U, which is hidden in the language, and plays a central role in the computational reasoning.
Lambda- S is an extension to first-order lambda calculus unifying two approaches of non-cloning in quantum lambda-calculi. One is to forbid duplication of variables, while the other is to consider all lambda-terms as algebraic linear functions. The type system of Lambda- S have a constructor S such that a type A is considered as the base of a vector space while S ( A ) is its span. A first semantics of this calculus have been given when first presented, with such an interpretation: superposed types are interpreted as vectors spaces while non-superposed types as their basis. In this paper we give a concrete categorical semantics of Lambda- S , showing that S is interpreted as the composition of two functors in an adjunction relation between the category of sets and the category of vector spaces over C . The right adjoint is a forgetful functor U , which is hidden in the language, and plays a central role in the computational reasoning.