In this work we introduce Qumin, a novel quantum programming language with a focus on providing an easy to use, minimalist, high-level, and easily extensible platform for quantum programming. Qumin's design concentrates on encompassing the various interactions between classical and quantum computation via the use of two sublanguages: an untyped one that handles classical preparation and control, and one linearly typed that explicitly handles quantum routines. This allows the classical part of the language to be freely used for general programming while placing restrictions on the quantum part that enforce rules of quantum computing like the no-cloning of qubits. We describe both the language's theoretical foundations in terms of lambda calculi and linear type systems, and more practical matters such as implementations of algorithms and useful programming tools like matrix and oracle generators that streamline the interaction of the classical and quantum fragments of a program. Finally, we provide an experimental open-source implementation of an interpreter, typechecker and related tools for the language (which can be found in this https URL ).
There also exist a number of imperative languages. To start with, we have the aforementioned works by Knill which includes an imperative-style pseudocode and with a full scheme and implementation in C++. One of the first attempts at writing a full imperative language, called QCL, is described by " O mer in @cite_17 , with a C-like syntax and high-level quantum programming features such as automatic memory management, user-defined operators, and automatic derivations of them. It also includes a classical sublanguage. Sanders and Zuliani @cite_24 have also proposed an imperative language, qGCL, which is based on a guarded command language and enjoys rigorous semantics and an associated refinement calculus. Another imperative language, LanQ, was introduced by Mlna r ' i k @cite_2 , who also provided operational semantics for it, as well as a type soundness proof for the non-communicating part of the language.
@cite_24 @cite_2 @cite_17
102856817 2034373223 2137628566 2157601714
We present an imperative quantum programming language LanQ which was designed to support combination of quantum and classical programming and basic process operations - process creation and interprocess communication. The language can thus be used for implementing both classical and quantum algorithms and protocols. Its syntax is similar to that of C language what makes it easy to learn for existing programmers. In this paper, we present operational semantics of the language and a proof of type soundness of the noncommunicating part of the language. We provide an example run of a quantum random number generator. We present a new approach to adding state and state-changing commands to a term language. As a formal semantics it can be seen as a generalization of predicate transformer semantics, but beyond that it brings additional opportunities for specifying and verifying programs. It is based on a construct called a phrase, which is a term of the form C r t, where C stands for a command and t stands for a term of any type. If R is boolean, C r R is closely related to the weakest precondition wp(C,R). The new theory draws together functional and imperative programming in a simple way. In particular, imperative procedures and functions are seen to be governed by the same laws as classical functions. We get new techniques for reasoning about programs, including the ability to dispense with logical variables and their attendant complexities. The theory covers both programming and specification languages, and supports unbounded demonic and angelic nondeterminacy in both commands and terms. In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions. We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive semantics of irreversible quantum computations realisable as quantum gates. QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings explicit. Strict programs are free from decoherence and hence preserve superpositions and entanglement -which is essential for quantum parallelism.