This paper introduces a novel abstraction for programming quantum operations, specifically projective Cliffords, as functions over the qudit Pauli group. Generalizing the idea behind Pauli tableaux, we introduce a type system and lambda calculus for projective Cliffords called LambdaPC, which captures well-formed Clifford operations via a Curry-Howard correspondence with a particular encoding of the Clifford and Pauli groups. Importantly, the language captures not just qubit operations, but qudit 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.

翻译：本文提出了一种新颖的量子操作编程抽象方法，特别针对投影Clifford操作，将其表示为量子比特Pauli群上的函数。通过推广Pauli表格背后的思想，我们引入了一种名为LambdaPC的类型系统和λ演算，用于描述投影Clifford操作。该语言通过Curry-Howard对应关系与特定编码的Clifford群和Pauli群相结合，从而捕获形式良好的Clifford操作。重要的是，该语言不仅适用于量子比特操作，还可推广至任意维度$d$的量子比特操作。全文通过多个示例以及专注于稳定子纠错码的案例研究，深入探讨了基于投影Clifford进行编程的内涵与实现方式。