Qudit Quantum Programming with Projective Cliffords

Abstract

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.