Programming with Projective Cliffords
summary
Defines a lambda calculus LambdaPC whose well‑typed functions are exactly projective Cliffords acting by conjugation on the Pauli group, proves a Curry-Howard correspondence, and shows how every such function compiles to a Clifford circuit by evaluating its action on the 2N Pauli basis and emitting a tableau. Types enforce linearity and preservation of the symplectic form, examples include a parametric swap, a poly→Clifford mapper, and a Steane code encoding with 7 data + 6 ancilla; compilation uses Poost.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:04Clifford operators and projective Cliffords
- 3:18Poly tableaux in stabilizer circuits
- 5:08Functional representation
- 8:17Polymorphic functions examples
- 10:06Steane code example
- 13:21Type system for verification
- 17:17Lambda πc calculus
- 18:42Why study Cliffords
- 20:40Q&A
related talks
45mLogic Meta Programming for Functional Languages
20mEnriched Presheaf Model of Quantum FPC
36mParallel Algebraic Effect Handlers
37mClassical Processes in modern dress
36mDependently Typed Multi-Stage Programming, Revisited
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
30mContinuations and Coexponentials
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders