A Graded Modal Type Theory for Pulse Schedules

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.