Granthi: Higher-Order Quantum Programming via Unitary Wiring
Samson Abramsky, Radha Jagadeesan
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了最后一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
它引用的顶会 Paper7
- Qunity: A Unified Language for Quantum and Classical ComputingFinn Voichick, Liyi Li, Robert Rand, Michael HicksPOPL 2023 · 被引用 35 次
- Twist: sound reasoning for purity and entanglement in Quantum programsCharles Yuan, Christopher McNally, Michael CarbinPOPL 2022 · 被引用 30 次
- Quantum Control Machine: The Limits of Control Flow in Quantum ProgrammingCharles Yuan, Agnes Villanyi, Michael CarbinOOPSLA 2024 · 被引用 9 次
- With a Few Square Roots, Quantum Computing Is as Easy as PiJacques Carette, Chris Heunen, Robin Kaarsgaard, Amr SabryPOPL 2024 · 被引用 7 次
- Qudit Quantum Programming with Projective CliffordsJennifer Paykin, Sam WinnickPOPL 2026 · 被引用 1 次
相关 Paper
- 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 次
- 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 次
