Granthi: Higher-Order Quantum Programming via Unitary Wiring
Samson Abramsky, Radha Jagadeesan
Abstract
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.
• Software and its engineering → Functional languages.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 77796c98-4f8d-4f22-9100-41716c13f9f2Builds on7
- Qunity: A Unified Language for Quantum and Classical ComputingFinn Voichick, Liyi Li, Robert Rand, Michael HicksPOPL 2023 · 35 citations
- Twist: sound reasoning for purity and entanglement in Quantum programsCharles Yuan, Christopher McNally, Michael CarbinPOPL 2022 · 30 citations
- Quantum Control Machine: The Limits of Control Flow in Quantum ProgrammingCharles Yuan, Agnes Villanyi, Michael CarbinOOPSLA 2024 · 9 citations
- With a Few Square Roots, Quantum Computing Is as Easy as PiJacques Carette, Chris Heunen, Robin Kaarsgaard, Amr SabryPOPL 2024 · 7 citations
- Qudit Quantum Programming with Projective CliffordsJennifer Paykin, Sam WinnickPOPL 2026 · 1 citation
Related papers
- Compositional Quantum Control Flow with Efficient Compilation in QunityMikhail Mints, Finn Voichick, Leonidas Lampropoulos, Robert RandOOPSLA 2025
- Linear Dependent Type Theory for Quantum Programming Languages: Extended AbstractPeng Fu, Kohei Kishida, Peter SelingerLICS 2020 · 23 citations
- Quantum Circuits Are Just a PhaseChris Heunen, Louis Lemonnier, Christopher McNally, Alex RicePOPL 2026
- Quantum Control and General Recursion Beyond the Unitary CaseKathleen Barsse, Romain Péchoux, Simon PerdrixLICS 2026
- Full abstraction for the quantum lambda-calculusPierre Clairambault, Marc de VismePOPL 2020 · 25 citations
