Research Article
A Survey of Quantum Type Theory: From Linearity to Formal Verification
@ARTICLE{10.4108/eetcasa.9669, author={Van Han Nguyen}, title={A Survey of Quantum Type Theory: From Linearity to Formal Verification}, journal={EAI Endorsed Transactions on Contex-aware Systems and Applications}, volume={10}, number={1}, publisher={EAI}, journal_a={CASA}, year={2025}, month={7}, keywords={Quantum Type Theory, Type Systems, Quantum Programming Languages,, Linear Logic, Dependent Types}, doi={10.4108/eetcasa.9669} }- Van Han Nguyen
Year: 2025
A Survey of Quantum Type Theory: From Linearity to Formal Verification
CASA
EAI
DOI: 10.4108/eetcasa.9669
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.
Copyright © 2025 Nguyen Van Han, licensed to EAI. This is an open access article distributed under the terms of the CC BY-NC-SA 4.0, which permits copying, redistributing, remixing, transformation, and building upon the material in any medium so long as the original work is properly cited.
