This paper introduces a novel abstraction for programming quantum operations, specifically projective Cliffords, as functions over the qudit Pauli group. We define a categorical semantics for projective Cliffords based on Pauli encodings in terms of $\mathbb{Z}_d$-linear maps. We then introduce a type system and lambda calculus for both $\mathbb{Z}_d$-linear maps and projective Cliffords, and prove that these type systems have a sound denotational semantics in terms of the relevant categories. Finally, we explore what it means to program with projective Cliffords through a number of examples and programming constructions.

翻译：本文提出了一种新颖的量子操作编程抽象方法，特别针对投影Clifford算符，将其视为量子比特泡利群上的函数。我们基于$\mathbb{Z}_d$线性映射的泡利编码，为投影Clifford算符定义了范畴语义。随后，我们为$\mathbb{Z}_d$线性映射和投影Clifford算符分别引入了类型系统和lambda演算，并证明这些类型系统在相关范畴中具有可靠的指称语义。最后，我们通过一系列示例和编程结构探讨了使用投影Clifford算符进行编程的实际意义。