Introducing BRAT
summary
BRAT is a functional language that interleaves quantum and classical code with linear qubit types, a kernel arrow for circuits and classical thunks for composable recipes. It shows a concrete magic state distillation pipeline using a 5‑qubit decoder, built‑in gates (H S T CNOT), vectorized maps over V 5, and a money resource type that enforces a constant qubit budget. Pattern matching on type‑level naturals makes kernel patterns irrefutable, an LSP with typed holes aids development, and currently BRAT is a type checker producing an internal graph but has no execution backend yet.
AI-written summary · about
chapters (11)
- 0:00BRAT language intro
- 1:52Motivation for BRAT
- 4:21BRAT syntax and functions
- 7:12Kernel vs classical types
- 9:23Classical functions with BRAT
- 11:35Pattern matching in BRAT
- 13:45Measuring syndrome in BRAT
- 15:59Managing cubits and money
- 17:27Magic state distillation in BRAT
- 19:33Future directions for BRAT
- 21:22BRAT status and next steps
related talks
26mQrisp: A Framework for Compilable High-Level Programming of Gate-Based Quantu...
17mAn Algebraic Language for Specifying Quantum Networks
16mqKleene: Verification of Quantum RAM Made Easy
14mA Language for Quantifying Quantum Network Behavior
40mQ# - going beyond quantum circuits
14mDependency-Aware Compilation for Surface Code Quantum Architectures
24mDeriving a Kronecker-Free Functional Quantum Simulator
15mToward A Quantum Programming Language for Higher Level Formal Verification