Programming with Projective Cliffords

Explore a 24-minute conference talk from PLanQC 2025 where Jennifer Paykin and Sam Winnick present an innovative approach to quantum programming. Learn about programming projective Cliffords directly through their conjugation action on Paulis, rather than traditional circuit-based methods. Discover LambdaPC, a lambda-calculus establishing a Curry-Howard correspondence where projective Cliffords are viewed as functions between Pauli types. The presentation explains how the type system combines linear types for vector transformations with orthogonality checks based on the symplectic form to encode Pauli group commutation relations. The speakers demonstrate that every Clifford can be represented in LambdaPC and efficiently synthesized into quantum circuits. This talk was presented at the PLanQC 2025 workshop on January 25, 2025, sponsored by ACM SIGPLAN.