Qudit Quantum Programming with Projective Cliffords
summary
Claims a lambda calculus called LambdaPC that encodes projective Cliffords as functions P ↦ UPU† for qudits of any dimension and proves expressiveness: every projective Clifford is representable. Implements a type system using linear types plus a condensed encoding that enforces mu and φ linearity and a symplectomorphism check (currently done via SMT), compiles well-typed terms to executable Clifford circuits, and demonstrates the approach on stabilizer error‑correcting codes with a working GitHub prototype.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:00Projective Cliffords as automorphisms
- 3:33Lambda PC language
- 8:10Clifford circuit compilation
- 11:19Lifting polies to Cliffords
- 15:54Extending to cudits
- 21:21Type system
- 23:08Case studies
- 24:15Q&A
related talks
23mA feasible and unitary programming language with quantum control
17mToward a Type Theoretic Interpretation of Q# and Statically Enforcing the No Cloning Theorem
30mDependently Typed Quantum Programming in Proto-Quipper
21mToward Certified Quantum Programming
24mAdventures in Qutrit Compilation
58mLimitations for Quantum PCPs
24mQunity: A Unified Language for Quantum and Classical Computing
15mToward A Quantum Programming Language for Higher Level Formal Verification