Document Open Access Logo

Linear Lambda-Calculus is Linear

Authors Alejandro Díaz-Caro , Gilles Dowek

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.21.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

Funding

STIC-AmSud 21STIC10, ECOS-Sud A17C03, and the French-Argentinian IRP SINFIN.
  • Díaz-Caro, Alejandro: PIP 11220200100368CO and PICT-2019-1272.

Acknowledgements

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 As Get 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) https://doi.org/10.4230/LIPIcs.FSCD.2022.21

Abstract

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
Keywords
  • Proof theory
  • Lambda calculus
  • Linear logic
  • Quantum computing

Metrics

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

Related Versions

References

  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: https://doi.org/10.1017/9781316219317.
  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: https://arxiv.org/abs/2012.08994.
  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
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact