Linear dependent type theory for quantum programming languages: extended abstract

DOI10.1145/3373718.3394765zbMATH Open1503.68039arXiv2004.13472OpenAlexW3020955609WikidataQ114020604 ScholiaQ114020604MaRDI QIDQ5043587FDOQ5043587

Authors: Peng Fu, Kohei Kishida, 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)

Abstract: Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.

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

Recommendations

• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• A categorical model for a quantum circuit description language (extended abstract)
• A lambda calculus for quantum computation with classical control
• QWIRE: a core language for quantum circuits

zbMATH Keywords

fibrationcategorical semanticscategorical modelquantum programming languageslinear dependent types

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Categorical logic and type theory
• Quantum computation and quantum information. 10th anniversary edition
• Title not available (Why is that?)
• Title not available (Why is that?)
• A lambda calculus for quantum computation with classical control
• Linear logic
• Bounded linear logic: A modular approach to polynomial-time computability
• Some properties of Fib as a fibred \(2\)-category
• Locally cartesian closed categories and type theory
• Title not available (Why is that?)
• An introduction to quantum programming in Quipper
• Title not available (Why is that?)
• Framed bicategories and monoidal fibrations
• A linear logical framework
• Linear dependent types for differential privacy
• QWIRE: a core language for quantum circuits
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• A categorical model for a quantum circuit description language (extended abstract)
• A categorical semantics for linear logical frameworks
• Integrating linear and dependent types
• A tutorial introduction to quantum circuit programming in dependently typed proto-quipper
• I got plenty o' nuttin'
• Syntax and semantics of quantitative type theory
• How nice are free completions of categories?
• \(\mathcal{Q}\)\textsc{wire} practice: formal verification of quantum circuits in Coq
• Title not available (Why is that?)

Uses Software

• Haskell
• Quipper
• Proto-Quipper-M

This page was built for publication: Linear dependent type theory for quantum programming languages: extended abstract

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5043587)