A Survey of Quantum Type Theory: From Linearity to Formal Verification

Van Han Nguyen

doi:10.4108/eetcasa.9669

Authors

Van Han Nguyen Thuyloi University

DOI:

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

Keywords:

Quantum Type Theory, Type Systems, Quantum Programming Languages,, Linear Logic, Dependent Types

Abstract

Quantum Type Theory (QTT) provides a formal system that combines ideas from quantum mechanics, type theory, and logic to support reliable quantum programming. Since quantum information cannot be copied or deleted like classical data, QTT uses linear types to ensure that quantum operations follow the laws of physics. This paper reviews the main concepts in QTT, such as linear functions, tensor products, and dependent types, and explains how they help programmers write safe and correct quantum code.

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 (LICS), pages 415–425, 2004.

[2] Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. Technical Report UCAM-CLTR- 352, University of Cambridge, Computer Laboratory, 1994.

[3] Benjamin Bichsel, Michael Baader, Timon Gehr, and Martin Vechev. Silq: A high-level quantum language with safe uncomputation and intuitive semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 286–300. ACM, 2020.

[4] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1–101, 1987.

[5] Jennifer Paykin, Robert Rand, and Steve Zdancewic. Qwire: a core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 846–858. ACM, 2017.

[6] Neil J. Ross and Peter Selinger. Quantum programming using the proto-quipper language. In Lecture Notes in Computer Science (TQC 2014), volume 8401, pages 119–132. Springer, 2014.

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

[8] 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.

[9] Sam Staton. Algebraic effects, linearity, and quantum programming languages. In LICS ’15: 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1–9. IEEE, 2015.

[10] Dominique Unruh. Quantum relational hoare logic. Logical Methods in Computer Science, 16(4):1–48, 2020.

[11] André van Tonder. A lambda calculus for quantum computation. SIAM Journal on Computing, 33(5):1109–1135, 2004.