A Graded Modal Type Theory for Pulse Schedules
Robin Adams
TL;DR
This work addresses the need for precise semantics of pulse schedules in superconducting quantum hardware by introducing PSTT, a graded modal type theory that encodes timing via timing grades like $x^d$. It develops a category-theoretic semantics using a symmetric monoidal category with a $\mathbb{Z}$-action to interpret types, terms, and gates, and presents two concrete models (input channels and chip trajectories) to validate the interpretation. The paper provides formal syntax, metatheory, and semantic results, including soundness and completeness via a syntactic initial model, enabling static guarantees that schedules are complete (no overlaps or gaps). This framework supports formally verified quantum compilation and precise reasoning about pulse schedules, with potential to improve reliability and verification of quantum software stacks.
Abstract
We propose a language for representing the pulse schedules that a superconducting quantum computer accepts as input. The language is a graded modal type theory named PSTT (Pulse Schedule Type Theory). Graded modals type theories are type systems where each variable is annotated with a parameter or grade. These can be used to represent, for example, resource usage, where the grade denotes how many times a given resource may be used; or privacy levels, whether a resource is private or public. In this system, we use the grades to represent timing information. We give categorical semantics to the system and prove soundness and completeness.