Programming Quantum Circuits in Proto-Quipper
Frank Fu
Computer Science and Engineering Department, University of South Carolina

Objectives of Proto-Quipper• Provide formal foundations for high-level quantum
programming languages.
• Identify high-level programming constructs forquantum circuits.
• Support programming a wide range of quantum
algorithms.

Introduction
Quipper is a functional programming language for quantum
computing. Proto-Quipper is a family of languages aiming toprovide a formal foundation for Quipper. We added a notionof dependent types to Proto-Quipper in 2020, which enables
Proto-Quipper to express family of quantum circuits indexedby parameters. Recently, we have extended Proto-Quipper
with a construct called dynamic lifting. Dynamic lifting is anoperation that enables a state, such as the result of a measurement, to be lifted to a parameter, where it can influence
the generation of the next portion of the circuit. As a result,dynamic lifting enables Proto-Quipper programs to interleaveclassical and quantum computation.

A Repeat-Until-Success Algorithm
The repeat-until-success paradigm provides a technique to apply a unitary that cannot be implemented exactly, at the costof potentially running the same circuit multiple times. In order to apply a non-Clifford+T gate N to a target qubit |ϕ⟩,one first initializes several ancillary qubits before applying awell-chosen Clifford+T circuit C to the target and the ancillas
and measuring the ancillas. If all of the measurement results
are 0, the target qubit is guaranteed to be in the state N |ϕ⟩.
Otherwise, a correction is applied to the target to return it to
its initial state and the process is repeated.
The following circuit gives an illustration of how to implement√the gate V3 = I+2iZ[Paetznick and Svore 2014].
5T0HT*0THHZMeasTHMeasQuantum Fourier Transform
The quantum Fourier transform is the map defined by|a1, . . . , an⟩ 7→(|0⟩ + e2πi0.a1a2...an |1⟩) . . . (|0⟩ + e2πi0.an−1an |1⟩)(|0⟩ + e2πi0.an |1⟩).
n/22Let us define the controlled rotation gates R(k) by
100 0
0 1 00.
R(k) = 0 0 10
2πi/2k000eApplying the Hadamard gate to the first qubit produces thefollowing state1
H1|a1, . . . , an⟩ = √ (|0⟩ + e2πi0.a1 |1⟩) ⊗ |a2, . . . , an⟩,2where the subscript on the gate indicates the qubit on which
the gate acts. We then apply a sequence of controlled rotations
using the the first qubit as the target. This yields
R(n)1,n . . . R(2)1,2H1|a1, . . . , an⟩ =Proto-Quipper Program for V3
The following is a Proto-Quipper program that implements therepeat-until-success algorithm for V3 gate outlined above.

Summary and Future Work12

2πi0.a1a2...an(|0⟩+e|1⟩)⊗|a2, . . . , an⟩,
1/2

where the subscripts i and j in R(k)i,j indicate the target andcontrol qubit, respectively. The following circuit corresponds
to QFT on 5 qubits.
HR(2)

R(3)

R(4)

We show Proto-Quipper programs for a repeat-until-success algorithm and Quantum Fourier Transform. They showcase theuse of dynamic lifting and dependent types. For future work,on the aspect of language design, we are investigating the support for controlling and reversing quantum circuits in ProtoQuipper. On the aspect of implementation and compilation,
we plan to explore the possibility of compiling Proto-Quipper
to lower level languages such as OpenQASM and QIR.

References[1] Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger.
Proto-quipper with dynamic lifting.
Proc. ACM Program. Lang., 7(POPL), jan 2023.
[2] Peng Fu, Kohei Kishida, and Peter Selinger.
Linear Dependent Type Theory for Quantum Programming
Languages.
Logical Methods in Computer Science, Volume 18, Issue 3,September 2022.
[3] Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger.
A tutorial introduction to quantum circuit programming independently typed Proto-Quipper.
In Proceedings of the 12th International Conference on Reversible
Computation, RC 2020, Oslo, Norway, volume 12227 of Lecture
Notes in Computer Science, pages 153–168. Springer, 2020.

R(5)

H

R(2)

R(3)

R(4)
H

R(2)

R(3)
H

R(2)
H

Acknowledgements
Joint work with Kohei Kishida, Neil J. Ross and Peter Selinger.

QFT in Proto-Quipper
The following is a Proto-Quipper program describes QFT as afamily of circuits parameterized by the number of qubits.

Contact Information• Gitlab repository:
https://gitlab.com/frank-peng-fu/dpq-remake• Web: https://cse.sc.edu/~pfu• Email: pfu@cse.sc.edu