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.