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

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

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationReversible Computation - 12th International Conference, RC 2020, Proceedings
Subtitle of host publication12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings
EditorsIvan Lanese, Mariusz Rawski
PublisherSpringer
Pages153-168
Number of pages16
ISBN (Print)9783030524814
DOIs
StatePublished - Jul 9 2020
Event12th International Conference on Reversible Computation,RC 2020 - Oslo, Norway
Duration: Jul 9 2020Jul 10 2020

Publication series

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

Conference

Conference12th International Conference on Reversible Computation,RC 2020
CountryNorway
CityOslo
Period7/9/207/10/20

Keywords

  • Linear dependent types
  • Proto-Quipper-D
  • Quantum programming languages

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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