Abstract Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms.
Abstract Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms.
Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit. Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex and practical quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this paper, we present Proto-Quipper-R, a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. We also show that our approach is expressive enough to verify realistic quantum algorithms.
Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quantum circuit . Since these programs can leverage all the expressive power of high-level classical languages, circuit description languages have been successfully used to describe complex quantum algorithms, whose circuits, however, may involve many more qubits and gate applications than current quantum architectures can actually muster. In this article, we present Proto-Quipper-R , a circuit description language endowed with a linear dependent type-and-effect system capable of deriving parametric upper bounds on the width of the circuits produced by a program. We prove both the standard type safety results and that the resulting resource analysis is correct with respect to a big-step operational semantics. Lastly, we introduce QuRA , a static analysis tool based on Proto-Quipper-R ’s type system, and use it to show that our framework allows for the automatic width verification of realistic quantum algorithms, such as the QFT and Grover’s algorithm.
We introduce a type system for the Quipper language designed to derive upper bounds on the size of the circuits produced by the typed program. This size can be measured according to various metrics, including width , depth and gate count , but also variations thereof obtained by considering only some wire types or some gate kinds. The key ingredients for achieving this level of flexibility are effects and refinement types, both relying on indices , that is, generic arithmetic expressions whose operators are interpreted differently depending on the target metric. The approach is shown to be correct through logical predicates, under reasonable assumptions about the chosen resource metric. This approach is empirically evaluated through the QuRA tool, showing that, in many cases, inferring tight bounds is possible in a fully automatic way.
This thesis contains contributions to the mathematical foundations of quantum programming languages. The likely arrival of scalable quantum computers in the not-so-distant future has resulted in a flurry of activity in the development of quantum programming languages. As in classical computing, the transition from a description of a quantum algorithm found in the literature to a hardware-specific set of instructions run on a quantum device is a complex process, prone to errors. This issue is exacerbated in the quantum setting not only by the complexity of quantum algorithms but also by the fragility of quantum information, which renders ineffective some of the classical techniques used to debug programs. In this thesis, we contribute to the solution of some of these issues. We introduce Proto-Quipper-M, a new quantum programming language designed to serve as a testbed for the research and development of sound mathematical semantics and reasoning techniques for quantum programs. We first present Proto-Quipper-M as a formalization of a fragment of Quipper, a high-level functional programming language for describing families of quantum circuits. In particular, we define Proto-Quipper-M as a simply-typed lambda calculus with a special type for quantum circuits and a strong type system designed to enforce linearity on quantum data, and thus prevent violations of the no-cloning property of quantum information. We endow Proto-Quipper-M with computational meaning via a big-step operational semantics and prove that the language is type-safe by showing that it enjoys the type-preservation and error-freeness properties. We also give Proto-Quipper-M a denotational semantics in a suitable class of monoidal categories and show that these categories give rise to linear-non-linear models in the sense of Benton, and thus models of intuitionistic linear logic. Finally, we crystallize the connection between the syntax and the semantics of the language by proving the soundness theorem for Proto-Quipper-M.
We consider a formal model of quantum circuit description languages (QCDLs) in which semantically meaningful programs correspond to computable unitary matrices. We show that any semantically universal QCDL -- that is, any QCDL able to describe all computable unitary matrices, which in turn form the set of matrices we can meaningfully represent on digital hardware -- cannot have a semi-decidable set of semantically meaningful descriptions. In particular, no such language admits a compiler that reliably recognizes all valid program descriptions. This result stands in contrast to classical programming languages. While compilation in languages such as C or C++ may itself involve non-terminating computations, the set of semantically meaningful programs remains recursively enumerable, since successful compilation provides a witness of validity. The essential difference lies in the nature of the semantic domains: classical languages describe partial recursive functions, whereas QCDLs describe total unitary operators. Our analysis establishes a fundamental limitation of quantum circuit description languages and highlights a structural distinction between classical and quantum models of computation at the level of formal language theory.
Modern quantum programming languages integrate quantum resources and classical control. They must, on the one hand, be linearly typed to reflect the no-cloning property of quantum resources. On the other hand, high-level and practical languages should also support quantum circuits as first-class citizens, as well as families of circuits that are indexed by some classical parameters. Quantum programming languages thus need linear dependent type theory. This paper defines a general semantic structure for such a type theory via certain fibrations of monoidal categories. The categorical model of the quantum circuit description language Proto-Quipper-M by Rios and Selinger (2017) constitutes an example of such a fibration, which means that the language can readily be integrated with dependent types. We then devise both a general linear dependent type system and a dependently typed extension of Proto-Quipper-M, and provide them with operational semantics as well as a prototype implementation.