A Review of Quantum Lambda Calculi: Linearity, Semantics, and Programming Models

Tran Ngoc Dan; Nguyen Thi Kim Phung; Nguyen Thi Hong Tu; Nguyen Van Han

doi:10.4108/eetcasa.9668

Authors

Tran Ngoc Dan Thuyloi University
Nguyen Thi Kim Phung Thuyloi University
Nguyen Thi Hong Tu Thuyloi University
Nguyen Van Han Thuyloi University

DOI:

https://doi.org/10.4108/eetcasa.9668

Keywords:

Quantum Lambda Calculus, Quantum Programming Lanugages, Quantum Circuits , Formal Semantics

Abstract

Quantum lambda calculi extend classical lambda calculus to model quantum computation by integrating linear types, quantum operations, and classical control. This paper surveys key calculi—including QΛ, QLC, Proto-Quipper, and QML—highlighting their design principles, type systems, and semantic foundations. By comparing their approaches to handling quantum data, control flow, and circuit construction, we provide insights into the current state and future directions of quantum programming language research.

References

[1] Samson Abramsky and Bob Coecke. A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pages 415–425, 2004.

[2] Thorsten Altenkirch and James Grattage. A functional quantum programming language. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 249–258. IEEE, 2005.

[3] Thorsten Altenkirch, James Grattage, and Amr Sabry. Qml: Quantum functional programming. Mathematical Structures in Computer Science, 21(2):233–246, 2011.

[4] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. Logic in Computer Science, 1994. LICS’94. Proceedings., Ninth Annual IEEE Symposium on, pages 121–130, 1994.

[5] Dan R. Ghica and Aleksandar Smith. Geometry of interaction for a quantum programming language. Logical Methods in Computer Science, 16(2), 2020.

[6] Alexander S. Green, Peter L. Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A scalable quantum programming language. ACM SIGPLAN Notices, 48(6):333–342, 2013. https://arxiv.org/abs/ 1304.3390.

[7] Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 10th anniversary edition edition, 2010.

[8] Neil J. Ross. Verified compiling for a functional quantum language. PhD thesis, Dalhousie University, 2015. https: //dalspace.library.dal.ca/handle/10222/73503.

[9] Amr Sabry. Modeling quantum computing in haskell. Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 100–112, 2003.

[10] Peter Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004.

[11] Peter Selinger. Dagger compact closed categories and completely positive maps. Electronic Notes in Theoretical Computer Science, 170:139–163, 2007.

[12] Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16(3):527–552, 2006. https://arxiv.org/abs/quant-ph/0603065.

[13] Sam Staton. Algebraic effects for quantum computation. Electronic Proceedings in Theoretical Computer Science, 195:357–374, 2015. Andris van Tonder. A lambda calculus for quantum computation. PhD thesis, University of Oxford, 2004. https://arxiv.org/abs/quant-ph/0401147.

[15] Juliana K Vizzotto, Thorsten Altenkirch, and Amr Sabry. Structuring quantum effects: superoperators as monads. Electronic Notes in Theoretical Computer Science, 176:303– 319, 2006.

[16] Philip Wadler. Linear types can change the world! Programming Concepts and Methods, pages 561–581, 1993.