发表机构
University College London; DePaul University（伦敦大学学院; 德保罗大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出纯酉高阶量子编程语言Granthi，基于三项设计承诺实现量子程序的高阶特性，可将良型项编译为量子电路，支持量子开关等功能。
AI 中文摘要
现有量子编程语言将高阶结构限制在经典宿主中，同时将量子层限制为对量子比特的一阶操作。本文提出Granthi，一种纯酉高阶量子编程语言，其基于三项设计承诺：量子程序是一等值，可被传递、返回和相干组合；加法结构是保留标记的路由而非观测分支，因此控制可保持在叠加态；面向程序员的有限标记类型及命名可逆操作提供领域级控制空间，无需暴露标记管理。每个良型项（包括函数类型项）在其边界接口上表示一个酉算子，编译器将其布线精确实现为物理量子比特布局上的量子电路（假设pytket后端正确）。Granthi实现为端到端系统：OCaml领域特定语言（DSL）通过无绑定核心中间表示（IR）经pytket细化表面程序，生成可执行量子电路。该语言直接支持编译为静态电路的量子开关，以及控制流历史上的干涉和结构化有限控制，所有功能均在纯酉片段内实现。
英文摘要
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
CommentsOOPSLA 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
