A Graded Modal Type Theory for Pulse Schedules
summary
Provides a pair of linearly typed languages with semantics in symmetric monoidal categories: a plain circuit language and Grampus, an annotated language that attaches integer time grades (e.g. Hadamard 110 ns, single-qubit 100 ns, two-qubit 500 ns) so inputs 610 ns and 600 ns in the past yield a now state. Builds semantics, constructs models from syntax, proves soundness and completeness, exposes a delay operation for nontrivial waits, and aims for a verified compiler whose hardware-model commutativity condition checks realizability.
AI-written summary · about
chapters (8)
- 0:00Grampus language intro
- 4:00Graded modal type theory basics
- 7:16Typing rules and quantum gates
- 9:24Semantics in Hilbert spaces
- 12:40Annotated language and timing
- 14:52Soundness, completeness, hardware models
- 15:58Future work and conclusion
- 16:25Q&A
related talks
49mQuantitative program reasoning in Granule via graded modal types
20mTowards Graded Modal Dependent Types
12mA Unified View of Modalities in Type Systems
27mPractical Extensions for Graded Monads
20mPulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
19mCombining Dependency, Grades, and Adjoint Logic
34mGraded Monads and Type-Level Programming for Dependence Analysis