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.
Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
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 -