The Proto-Quipper family of programming languages aims to provide a formal foundation for the Quipper quantum programming language. Unfortunately, Proto-Quipper languages have complex operational semantics: they are inherently effectful, and they rely on set-theoretic operations and fresh name generation to manipulate quantum circuits. This makes them difficult to reason about using standard programming language techniques and, ultimately, to mechanize. We introduce Proto-Quipper-A, a rational reconstruction of Proto-Quipper languages for static circuit generation. It uses a linear $λ$ -calculus to describe quantum circuits with normal forms that closely correspond to box-and-wire circuit diagrams. Adjoint-logical foundations integrate this circuit language with a linear/non-linear functional language and let us reconstruct Proto-Quipper's circuit programming abstractions using more primitive adjoint-logical operations. Proto-Quipper-A enjoys a simple call-by-value reduction semantics, and to illustrate its tractability as a foundation for Proto-Quipper languages, we show that it is normalizing. We show how to use standard logical relations to prove normalization of linear and substructural systems, thereby avoiding the inherent complexity of existing linear logical relations.The Proto-Quipper family of programming languages aims to provide a formal foundation for the Quipper quantum programming language. Unfortunately, Proto-Quipper languages have complex operational semantics: they are inherently effectful, and they rely on set-theoretic operations and fresh name generation to manipulate quantum circuits. This makes them difficult to reason about using standard programming language techniques and, ultimately, to mechanize. We introduce Proto-Quipper-A, a rational reconstruction of Proto-Quipper languages for static circuit generation. It uses a linear $λ$-calculus to describe quantum circuits with normal forms that closely correspond to box-and-wire circuit diagrams. Adjoint-logical foundations integrate this circuit language with a linear/non-linear functional language and let us reconstruct Proto-Quipper's circuit programming abstractions using more primitive adjoint-logical operations. Proto-Quipper-A enjoys a simple call-by-value reduction semantics, and to illustrate its tractability as a foundation for Proto-Quipper languages, we show that it is normalizing. We show how to use standard logical relations to prove normalization of linear and substructural systems, thereby avoiding the inherent complexity of existing linear logical relations.

arXiv:2510.20018Oct 22, 20251 citation

Quantum Programming: Languages and Frameworks

Ashwin Prakash Nalwade, Khan Shariya Hasan Upoma

Springer eBooksJan 1, 20260 citations

Foundations of Quantum Programming

Elsevier eBooksJan 1, 20249 citations

Five Quantum Algorithms Using Quipper

Safat Siddiqui, Mohammed Jahirul Islam, Omar Shehab

Quipper is a recently released quantum programming language. In this report, we explore Quipper's programming framework by implementing the Deutsch's, Deutsch-Jozsa's, Simon's, Grover's, and Shor's factoring algorithms. It will help new quantum programmers in an instructive manner. We choose Quipper especially for its usability and scalability though it's an ongoing development project. We have also provided introductory concepts of Quipper and prerequisite backgrounds of the algorithms for readers' convenience. We also have written codes for oracles (black boxes or functions) for individual algorithms and tested some of them using the Quipper simulator to prove correctness and introduce the readers with the functionality. As Quipper 0.5 does not include more than \ensuremath{4 \times 4} matrix constructors for Unitary operators, we have also implemented \ensuremath{8 \times 8} and \ensuremath{16 \times 16} matrix constructors.Quipper is a recently released quantum programming language. In this report, we explore Quipper's programming framework by implementing the Deutsch's, Deutsch-Jozsa's, Simon's, Grover's, and Shor's factoring algorithms. It will help new quantum programmers in an instructive manner. We choose Quipper especially for its usability and scalability though it's an ongoing development project. We have also provided introductory concepts of Quipper and prerequisite backgrounds of the algorithms for readers' convenience. We also have written codes for oracles (black boxes or functions) for individual algorithms and tested some of them using the Quipper simulator to prove correctness and introduce the readers with the functionality. As Quipper 0.5 does not include more than \ensuremath{4 \times 4} matrix constructors for Unitary operators, we have also implemented \ensuremath{8 \times 8} and \ensuremath{16 \times 16} matrix constructors.

arXiv:1406.4481Jun 17, 20144 citations

λ

-calculus to describe quantum circuits with normal forms that closely correspond to box-and-wire circuit diagrams. Adjoint-logical foundations integrate this circuit language with a linear/non-linear functional language and let us reconstruct Proto-Quipper's circuit programming abstractions using more primitive adjoint-logical operations. Proto-Quipper-A enjoys a simple call-by-value reduction semantics, and to illustrate its tractability as a foundation for Proto-Quipper languages, we show that it is normalizing. We show how to use standard logical relations to prove normalization of linear and substructural systems, thereby avoiding the inherent complexity of existing linear logical relations.