Linear Dependent Type Theory for Quantum Programming Languages

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

Peter Selinger, Kohei Kishida, Peng Fu

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

fibrationcategorical semanticscategorical modelquantum programming languageslinear dependent types

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Quantum computation (81P68) Theory of programming languages (68N15) Quantum algorithms and complexity in the theory of computing (68Q12) Monoidal categories, symmetric monoidal categories (18M05) Type theory (03B38)

Related Items

Linear Dependent Type Theory for Quantum Programming Languages ⋮ Semantics of quantum programming languages: Classical control, quantum control

Uses Software

• Haskell
• Quipper
• Proto-Quipper-M

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Bounded linear logic: A modular approach to polynomial-time computability
• Categorical logic and type theory
• Some properties of Fib as a fibred \(2\)-category
• A linear logical framework
• A tutorial introduction to quantum circuit programming in dependently typed proto-quipper
• How nice are free completions of categories?
• Integrating Linear and Dependent Types
• An Introduction to Quantum Programming in Quipper
• Linear dependent types for differential privacy
• A Categorical Semantics for Linear Logical Frameworks
• Quantum Computation and Quantum Information
• I Got Plenty o’ Nuttin’
• Locally cartesian closed categories and type theory
• A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)
• Framed bicategories and monoidal fibrations
• Linear Dependent Type Theory for Quantum Programming Languages
• Syntax and Semantics of Quantitative Type Theory
• QWIRE: a core language for quantum circuits
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• A lambda calculus for quantum computation with classical control