Linear Lambda-Calculus is Linear

Authors Alejandro Díaz-Caro , Gilles Dowek

Thumbnail PDF


  • Filesize: 0.7 MB
  • 17 pages

Document Identifiers

Author Details

Alejandro Díaz-Caro
  • Departamento de Ciencia y Tecnología, Universidad Nacional de Quilmes, Bernal, Buenos Aires, Argentina
  • Instituto de Ciencias de la Computación, CONICET / Universidad de Buenos Aires, Buenos Aires, Argentina
Gilles Dowek
  • Inria, Paris, France
  • ENS Paris-Saclay, France


The authors want to thank Thomas Ehrhard, Jean-Baptiste Joinet, Jean-Pierre Jouannaud, Dale Miller, Alberto Naibo, Simon Perdrix, Alex Tsokurov, and Lionel Vaux for useful discussions.

Cite AsGet BibTex

Alejandro Díaz-Caro and Gilles Dowek. Linear Lambda-Calculus is Linear. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Lambda calculus
  • Theory of computation → Linear logic
  • Theory of computation → Quantum computation theory
  • Proof theory
  • Lambda calculus
  • Linear logic
  • Quantum computing


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. T. Altenkirch and J. Grattage. A functional quantum programming language. In Proceedings of LICS 2005, pages 249-258. IEEE, 2005. Google Scholar
  2. P. Arrighi and G. Dowek. Lineal: A linear-algebraic lambda-calculus. Logical Methods in Computer Science, 13(1), 2017. Google Scholar
  3. R. Blute. Hopf algebras and linear logic. Mathematical Structures in Computer Science, 6(2):189-217, 1996. Google Scholar
  4. B. Coecke and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. URL:
  5. A. Díaz-Caro and G. Dowek. A new connective in natural deduction, and its application to quantum computing. In A. Cerone and P. Csaba Ölveczky, editors, Prooceedings of the International Colloquium on Theoretical Aspects of Computing, volume 12819 of Lecture Notes in Computer Science, pages 175-193. Springer, 2021. Long version accessible at URL:
  6. A. Díaz-Caro, M. Guillermo, A. Miquel, and B. Valiron. Realizability in the unitary sphere. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), pages 1-13, 2019. Google Scholar
  7. A. Díaz-Caro and O. Malherbe. Quantum control in the unitary sphere: Lambda-S₁ and its categorical model. Draft at arXiv:2012.05887, 2020. Google Scholar
  8. A. Díaz-Caro, G. Dowek, and J.P. Rinaldi. Two linearities for quantum computing in the lambda calculus. Biosystems, 2019. Google Scholar
  9. Th. Ehrhard. On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science, 12(5):579-623, 2002. Google Scholar
  10. J.-Y. Girard. Linear logic. Theoreoretical Computer Science, 50:1-102, 1987. Google Scholar
  11. J.-Y. Girard. Coherent banach spaces: A continuous denotational semantics. Theoretical Computer Science, 227(1-2):275-297, 1999. Google Scholar
  12. P. Selinger and B. Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16(3):527-552, 2006. Google Scholar
  13. L. Vaux. The algebraic lambda calculus. Mathematical Structures in Computer Science, 19(5):1029-1059, 2009. Google Scholar
  14. M. Zorzi. On quantum lambda calculi: a foundational perspective. Mathematical Structures in Computer Science, 26(7):1107-1195, 2016. Google Scholar