一句话：提出面向 qudit 的投影 Clifford 类型系统与 λPc 演算，经 Curry-Howard 对应编译为量子电路。
本文研究如何为量子操作提供编程抽象，特别是超越 qubit 的 qudit 操作。作者将 Pauli tableaux 的思想推广，提出投影 Clifford 的抽象，将其视为 qudit Pauli 群上的函数，并定义一个类型系统与 lambda 演算 λPc。λPc 通过 Curry-Howard 对应与 Clifford 群和 Pauli 群的特定编码相联系，从而刻画良构的 Clifford 操作。在该语言中，用户编写编码投影 Clifford 映射 P ↦ UPU† 的函数，这些函数被编译为可在现代量子计算机上执行的电路，将量子态 |φ⟩ 变换为 U|φ⟩，且允许相差全局相位。该语言不仅支持 qubit 操作，也支持任意维度 d 的 qudit 操作。作者通过若干示例以及一个聚焦稳定子纠错码的案例研究，探讨了用投影 Clifford 编程的含义。
This paper introduces a novel abstraction for programming quantum operations, specifically projective Cliffords , as functions over the qu d it Pauli group. Generalizing the idea behind Pauli tableaux, we introduce a type system and lambda calculus for projective Cliffords called λ P c that captures well-formed Clifford operations via a Curry-Howard correspondence with a particular encoding of the Clifford and Pauli groups. In λ P c , users write functions that encode projective Cliffords P ↦ UPU † , and such functions are compiled to circuits executable on modern quantum computers that transform quantum states | φ ⟩ into U | φ ⟩, up to a global phase. Importantly, the language captures not just qubit operations, but qu d it operations for any dimension d . Throughout the paper we explore what it means to program with projective Cliffords through a number of examples and a case study focusing on stabilizer error correcting codes.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{PaykinW26,
title = {Qudit Quantum Programming with Projective Cliffords},
author = {Jennifer Paykin and Sam Winnick},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776646}
}