Qudit Quantum Programming with Projective Cliffords

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 that captures well-formed Clifford operations via a Curry-Howard correspondence with a particular encoding of the Clifford and Pauli groups. In LambdaPC, users write functions that encode projective Cliffords P ↦ U P U † , 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 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.