Peng Fu ; Kohei Kishida ; Peter Selinger - Linear Dependent Type Theory for Quantum Programming Languages

lmcs:6930 - Logical Methods in Computer Science, September 7, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:28)2022
Linear Dependent Type Theory for Quantum Programming LanguagesArticle

Authors: Peng Fu ; Kohei Kishida ; Peter Selinger

    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.


    Volume: Volume 18, Issue 3
    Published on: September 7, 2022
    Accepted on: June 8, 2022
    Submitted on: November 30, 2020
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,Mathematics - Category Theory,Quantum Physics

    1 Document citing this article

    Consultation statistics

    This page has been seen 1600 times.
    This article's PDF has been downloaded 430 times.