Linear Dependent Type Theory for Quantum Programming Languages

DOI10.46298/lmcs-18(3:28)2022zbMath1503.68039arXiv2004.13472WikidataQ114020604 ScholiaQ114020604MaRDI QIDQ5043587

Kohei Kishida, Peng Fu, Peter Selinger

Publication date: 6 October 2022

Published in: Logical Methods in Computer Science, Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2004.13472

zbMATH Keywords

fibration; categorical semantics; categorical model; quantum programming languages; linear dependent types

Mathematics Subject Classification ID

68N19: Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

81P68: Quantum computation

68N15: Theory of programming languages

68Q12: Quantum algorithms and complexity in the theory of computing

18M05: Monoidal categories, symmetric monoidal categories

03B38: Type theory

Uses Software

• Haskell
• Quipper
• Proto-Quipper-M