A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper

Peng Fu; Kohei Kishida; Neil J. Ross; Peter Selinger

doi:10.1007/978-3-030-52482-1_9

A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger

Philosophy

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

Abstract

We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.

Original language	English (US)
Title of host publication	Reversible Computation - 12th International Conference, RC 2020, Proceedings
Subtitle of host publication	12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings
Editors	Ivan Lanese, Mariusz Rawski
Publisher	Springer
Pages	153-168
Number of pages	16
ISBN (Print)	9783030524814
DOIs	https://doi.org/10.1007/978-3-030-52482-1_9
State	Published - Jul 9 2020
Event	12th International Conference on Reversible Computation,RC 2020 - Oslo, Norway Duration: Jul 9 2020 → Jul 10 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12227 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Conference on Reversible Computation,RC 2020
Country	Norway
City	Oslo
Period	7/9/20 → 7/10/20

Keywords

Linear dependent types
Proto-Quipper-D
Quantum programming languages

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-030-52482-1_9

Fingerprint Dive into the research topics of 'A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper'. Together they form a unique fingerprint.

Cite this

Fu, P., Kishida, K., Ross, N. J., & Selinger, P. (2020). A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. In I. Lanese, & M. Rawski (Eds.), Reversible Computation - 12th International Conference, RC 2020, Proceedings: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings (pp. 153-168). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12227 LNCS). Springer. https://doi.org/10.1007/978-3-030-52482-1_9

A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. / Fu, Peng; Kishida, Kohei; Ross, Neil J.; Selinger, Peter.

Reversible Computation - 12th International Conference, RC 2020, Proceedings: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings. ed. / Ivan Lanese; Mariusz Rawski. Springer, 2020. p. 153-168 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12227 LNCS).

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

Fu, P, Kishida, K, Ross, NJ & Selinger, P 2020, A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. in I Lanese & M Rawski (eds), Reversible Computation - 12th International Conference, RC 2020, Proceedings: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12227 LNCS, Springer, pp. 153-168, 12th International Conference on Reversible Computation,RC 2020, Oslo, Norway, 7/9/20. https://doi.org/10.1007/978-3-030-52482-1_9

Fu P, Kishida K, Ross NJ, Selinger P. A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. In Lanese I, Rawski M, editors, Reversible Computation - 12th International Conference, RC 2020, Proceedings: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings. Springer. 2020. p. 153-168. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-52482-1_9

Fu, Peng ; Kishida, Kohei ; Ross, Neil J. ; Selinger, Peter. / A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. Reversible Computation - 12th International Conference, RC 2020, Proceedings: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings. editor / Ivan Lanese ; Mariusz Rawski. Springer, 2020. pp. 153-168 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3d0e4bc19e094aacbbfd6fdefdaa0918,

title = "A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper",

abstract = "We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.",

keywords = "Linear dependent types, Proto-Quipper-D, Quantum programming languages",

author = "Peng Fu and Kohei Kishida and Ross, {Neil J.} and Peter Selinger",

note = "Funding Information: 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.; 12th International Conference on Reversible Computation,RC 2020 ; Conference date: 09-07-2020 Through 10-07-2020",

year = "2020",

month = jul,

day = "9",

doi = "10.1007/978-3-030-52482-1_9",

language = "English (US)",

isbn = "9783030524814",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "153--168",

editor = "Ivan Lanese and Mariusz Rawski",

booktitle = "Reversible Computation - 12th International Conference, RC 2020, Proceedings",

}

TY - GEN

T1 - A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper

AU - Fu, Peng

AU - Kishida, Kohei

AU - Ross, Neil J.

AU - Selinger, Peter

N1 - Funding Information: 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.

PY - 2020/7/9

Y1 - 2020/7/9

N2 - We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.

AB - We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.

KW - Linear dependent types

KW - Proto-Quipper-D

KW - Quantum programming languages

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

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

U2 - 10.1007/978-3-030-52482-1_9

DO - 10.1007/978-3-030-52482-1_9

M3 - Conference contribution

AN - SCOPUS:85085950443

SN - 9783030524814

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 153

EP - 168

BT - Reversible Computation - 12th International Conference, RC 2020, Proceedings

A2 - Lanese, Ivan

A2 - Rawski, Mariusz

PB - Springer

T2 - 12th International Conference on Reversible Computation,RC 2020

Y2 - 9 July 2020 through 10 July 2020

ER -