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 \mapsto U P U^\dagger$, and such functions are compiled to circuits executable on modern quantum computers that transform quantum states $\ket{\varphi}$ into $U \ket{\varphi}$, 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.