We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeingboth unitarity and polynomial-time normalization. Unitarity is achieved by using a special modality forsuperpositions while requiring orthogonality among superposed terms. Polynomial-time normalization isachieved using a linear-logic-based type discipline employing Barber and Plotkin duality along with a specificmodality to account for potential duplications. This type discipline also guarantees that derived values havepolynomial size. Our language seamlessly combines the two modalities: quantum circuit programs upholdunitarity, and all programs are evaluated in polynomial time, ensuring their feasibility.
We introduce a novel quantum programming language featuring higher-order programs and quantum controlflow which ensures that all qubit transformations are unitary. Our language boasts a type system guaranteeingboth unitarity and polynomial-time normalization. Unitarity is achieved by using a special modality forsuperpositions while requiring orthogonality among superposed terms. Polynomial-time normalization isachieved using a linear-logic-based type discipline employing Barber and Plotkin duality along with a specificmodality to account for potential duplications. This type discipline also guarantees that derived values havepolynomial size. Our language seamlessly combines the two modalities: quantum circuit programs upholdunitarity, and all programs are evaluated in polynomial time, ensuring their feasibility.
Many mainstream quantum programming languages confine higher-order structure to a classical host while restricting the quantum layer to first-order operations on qubits. This paper presents Granthi, a purely unitary higher-order quantum programming language built on three design commitments: quantum programs are first-class values that may be passed, returned, and coherently composed; additive structure is tag-preserving routing rather than observational branching, so control may remain in superposition; and programmer-facing finite label types with staged reversible-operation bindings provide domain-level control spaces without exposing tag management. These bindings are eliminated by elaboration before Source typing.
Granthi deterministically normalizes each Source program to a canonical wiring form. Every well-typed Source program, including a term of function type, has a unitary boundary interpretation. Under backend correctness (BC), the reference compiler produces a unitary circuit realizing that interpretation.
Granthi's currently supported executable fragment is implemented end-to-end: an OCaml DSL elaborates surface programs through a higher-order Core IR to executable quantum circuits via pytket. The language directly supports the pure-unitary quantum switch for explicitly supplied operations; closed instances compile to static circuits. It also supports interference on control-flow history and structured finite control, all within the purely unitary fragment
qPCF is a paradigmatic quantum programming language that ex- tends PCF with quantum circuits and a quantum co-processor. Quantum circuits are treated as classical data that can be duplicated and manipulated in flexible ways by means of a dependent type system. The co-processor is essentially a standard QRAM device, albeit we avoid to store permanently quantum states in between two co-processor's calls. Despite its quantum features, qPCF retains the classic programming approach of PCF. We introduce qPCF syntax, typing rules, and its operational semantics. We prove fundamental properties of the system, such as Preservation and Progress Theorems. Moreover, we provide some higher-order examples of circuit encoding.
Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.
We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.
As quantum computing hardware advances toward practical implementation, the design of high-level programming languages for quantum-classical hybrid systems remains a critical challenge. Current quantum programming approaches lack unified abstractions that seamlessly integrate classical and quantum computation. This paper proposes a foundational framework for a high-level quantum-classical hybrid programming language based on multi-modal type theory. Our approach formulates quantum-classical hybrid computation as staged computation, where classical computation generates and executes quantum programs. We adapt type systems and operational semantics from prior research in classical staged computation to this framework. This research provides a theoretical foundation for implementing interpreters and compilers that uniformly handle both classical and quantum computation.
In contrast to a classical bit, which can only take the value 0 or 1, its quantum counterpart -- a qubit -- can exist in a superposition of 0 and 1. This is a superposition of data values, naturally raising the question of whether one can superpose not only data but also programs. For example, a particular superposition of programs, known as the quantum SWITCH, has attracted much attention, and its implementations and computational advantages have been studied extensively within the physics community.
A naive way to control a program by a qubit is by means of a controlled operation. Given an operation F, this amounts to considering an operation that behaves as F when the control qubit is ∣1⟩, and as the identity operation when the control qubit is ∣0⟩. This idea works well when F is a unitary operation, but it is not well-defined for a general quantum channel. By contrast, the quantum SWITCH is free from the well-definedness issue. This contrast leads to the key insight of this paper: controlled operations and the quantum SWITCH should be regarded as different kinds of quantum control mechanisms.
Building on this insight, we develop a novel quantum programming language with quantum control and measurement that can express the quantum SWITCH over quantum channels. Using a semantic analysis based on program transformations, we identify the source of the ill-behavedness of controlled operations as the \emph{correspondence problem}: a lack of coordination between the measurements performed in the then- and else-branches of quantum conditional branching. We address this problem with a linear type system that enforces alignment of the quantum operations used in the two branches, yielding a well-behaved language capable of expressing the quantum SWITCH.