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
Comments
OOPSLA 2026. v3. New version with a corrigendum (fixing a soundness error in the typing of sums), and revised proofs of an expanded formal treatment of the compiler (v 1.0.2). Implementation: https://github.com/radhajagadeesan/granthi
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
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 develop a boundary-centric semantic framework for higher-order quantum computation, building on the Kelly-Laplaza description of compact closure and Abramsky's execution account. In the semantic carrier Perm(C), morphisms are complex-linear combinations of polarized boundary linkings, composed by execution. Finite-family addresses provide coherent control over finite-level quantum registers (qudits) while retaining the multiplicative boundary structure.
We identify essential unitarity, a boundary condition extending ordinary unitarity to higher-order interfaces. On positive qudit registers it coincides with ordinary matrix unitarity; at higher order it expresses preservation of information across the full polarized boundary.
We define a unit-free coherent quantum core generated by multiplicative wiring, unitary gates on positive qudit registers, and contextual coherent control, and prove that every one of its morphisms is essentially unitary. The framework realizes an applied coherent quantum switch and the unitary stages of equal-ratio one-slot supermap dilations with explicit memory.
An extended abstract of this work was accepted for QPL 2026 and is forthcoming in its proceedings.
We present a new quantum programming language called ‘Qualia’ that enables transparent programming of quantum hardware. Qualia allows seamless integration of abstraction layers such as the digital circuit layer and the analog control pulse waveform layer. Additionally, the language supports user-issued low-level hardware instructions like FPGA actions. Mid-circuit measurements and branching decision logic support real-time, adaptive programs. This flexibility allows users to write code for everything from quantum error correction to analog quantum simulation. The combination of a user-facing calibration database and a powerful symbolic algebra framework provides users with an unprecedented level of expressiveness and transparency. We display the salient characteristics of the language structure and describe how the accompanying compiler can translate programs written in any abstraction layer into precisely timed hardware commands. Qualia provides a fully transparent programming interface that allows simultaneous circuit level and hardware level control. There is no "behind-the-scenes" circuit compilation or hardware calibration. Every command is executed exactly as the the user dictates.
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.
Bloch is a modern quantum programming language and interpreter designed to feel familiar to systems developers while remaining hardware-agnostic.The project combines a statically typed surface language, a semantic analyser that guards against classical/quantum misuse before execution, and an interpreter that emits OpenQASM traces and aggregates multi-shot measurement results.Bloch supports classical control flow, deterministic resource management, and first-class annotations such as @quantum (to delineate quantum code) and @tracked (to stream measurements into probability tables).The language is implemented in C++20, ships with a comprehensive test suite, and is licensed under Apache-2.0to encourage adoption in research and industrial workflows.By pairing static semantics with vendor-neutral QASM emission, Bloch targets the gap between dynamically typed Python-first SDKs (e.g., Qiskit and Cirq (Cirq Developers, 2023; Qiskit contributors, 2023)) and vendor-specific languages while keeping a single-binary, non-Python toolchain.
Quantum programs today are written at a low level of abstraction—quantum circuits akin to assembly languages—and the unitary parts of even advanced quantum programming languages essentially function as circuit description languages. This state of affairs impedes scalability, clarity, and support for higher-level reasoning. More abstract and expressive quantum programming constructs are needed. To this end, we introduce a simple syntax for generating unitaries from “just a phase”; we combine a (global) phase operation that captures phase shifts with a quantum analogue of the “if let” construct that captures subspace selection via pattern matching. This minimal language lifts the focus from gates to eigendecomposition, conjugation, and controlled unitaries; common building blocks in quantum algorithm design. We demonstrate several aspects of the expressive power of our language in several ways. Firstly, we establish that our representation is universal by deriving a universal quantum gate set. Secondly, we show that important quantum algorithms can be expressed naturally and concisely, including Grover’s search algorithm, Hamiltonian simulation, Quantum Fourier Transform, Quantum Signal Processing, and the Quantum Eigenvalue Transformation. Furthermore, we give clean denotational semantics grounded in categorical quantum mechanics. Finally, we implement a prototype compiler that efficiently translates terms of our language to quantum circuits, and prove that it is sound with respect to these semantics. Collectively, these contributions show that this construct offers a principled and practical step toward more abstract and structured quantum programming.