Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract

Peng Fu; Kohei Kishida; Peter Selinger

doi:10.1145/3373718.3394765

Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract

Peng Fu, Kohei Kishida, Peter Selinger

Philosophy

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 in [28] 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.

Original language	English (US)
Title of host publication	Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Subtitle of host publication	Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
Publisher	Association for Computing Machinery
Pages	440-453
Number of pages	14
ISBN (Electronic)	9781450371049
ISBN (Print)	9781450371049
DOIs	https://doi.org/10.1145/3373718.3394765
State	Published - Jul 8 2020
Event	Annual ACM/IEEE Symposium on Logic in Computer Science - Saarbrücken, Germany Duration: Jul 8 2020 → Jul 11 2020 Conference number: 35

Publication series

Name	ACM International Conference Proceeding Series

Conference

Conference	Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2020
Country/Territory	Germany
City	Saarbrücken
Period	7/8/20 → 7/11/20

Keywords

Quantum programming languages
categorical model
fibration
linear dependent types

ASJC Scopus subject areas

Software
Human-Computer Interaction
Computer Vision and Pattern Recognition
Computer Networks and Communications

Online availability

10.1145/3373718.3394765

Library availability

Discover UIUC Full Text

Cite this

Fu, P., Kishida, K., & Selinger, P. (2020). Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 440-453). Article 3394765 (ACM International Conference Proceeding Series). Association for Computing Machinery. https://doi.org/10.1145/3373718.3394765

Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. / Fu, Peng; Kishida, Kohei; Selinger, Peter.
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery, 2020. p. 440-453 3394765 (ACM International Conference Proceeding Series).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Fu, P, Kishida, K & Selinger, P 2020, Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science., 3394765, ACM International Conference Proceeding Series, Association for Computing Machinery, pp. 440-453, Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, 7/8/20. https://doi.org/10.1145/3373718.3394765

Fu P, Kishida K, Selinger P. Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery. 2020. p. 440-453. 3394765. (ACM International Conference Proceeding Series). doi: 10.1145/3373718.3394765

Fu, Peng ; Kishida, Kohei ; Selinger, Peter. / Linear Dependent Type Theory for Quantum Programming Languages : Extended Abstract. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. Association for Computing Machinery, 2020. pp. 440-453 (ACM International Conference Proceeding Series).

@inproceedings{e39582edc867446a8d1bd9397786799d,

title = "Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract",

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 in [28] 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.",

keywords = "Quantum programming languages, categorical model, fibration, linear dependent types",

author = "Peng Fu and Kohei Kishida and Peter Selinger",

note = "Funding Information: We thank Neil J. Ross for helpful discussions of a draft of this paper, and Marco Gaboardi and Aaron Stump for pointing out related works. This work was supported by the Air Force Office of Scientific Research under award number FA9550-15-1-0331. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the U.S. Department of Defense.; Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 ; Conference date: 08-07-2020 Through 11-07-2020",

year = "2020",

month = jul,

day = "8",

doi = "10.1145/3373718.3394765",

language = "English (US)",

isbn = "9781450371049",

series = "ACM International Conference Proceeding Series",

publisher = "Association for Computing Machinery",

pages = "440--453",

booktitle = "Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020",

address = "United States",

}

TY - GEN

T1 - Linear Dependent Type Theory for Quantum Programming Languages

T2 - Annual ACM/IEEE Symposium on Logic in Computer Science

AU - Fu, Peng

AU - Kishida, Kohei

AU - Selinger, Peter

N1 - Conference code: 35

PY - 2020/7/8

Y1 - 2020/7/8

N2 - 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 in [28] 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.

AB - 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 in [28] 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.

KW - Quantum programming languages

KW - categorical model

KW - fibration

KW - linear dependent types

UR - http://www.scopus.com/inward/record.url?scp=85085948833&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85085948833&partnerID=8YFLogxK

U2 - 10.1145/3373718.3394765

DO - 10.1145/3373718.3394765

M3 - Conference contribution

SN - 9781450371049

T3 - ACM International Conference Proceeding Series

SP - 440

EP - 453

BT - Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020

PB - Association for Computing Machinery

Y2 - 8 July 2020 through 11 July 2020

ER -

Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this