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.

@article{paperbot3935,
  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}
}