A Graded Modal Type Theory for Pulse Schedules

The operations to be performed by a quantum computer are almost invariably given in the form of a quantum circuit. In the final stage of compilation, a quantum circuit must be translated into the input signals accepted by the quantum hardware itself. For a quantum computer based on superconducting qubits, this will be a sequence of microwave control pulses to be sent to the various input channels. A pulse schedule gives a full specification for which pulse should be applied to which channel at what time. There is as yet no language for these pulse schedules that is very amenable to formal semantics. In this paper, we propose such a language called GRAMPUS (GRAded Modal type theory for PUlse Schedules). It is a graded modal type theory, where the grades represent timing information: a variable $x :^{50} Q_1$ will represent a state of qubit $Q_1$ that will exist 50 nanoseconds in the future, and a variable $y :^{-75} Q_2$ will represent a state of qubit $Q_2$ that existed 75 nanoseconds in the past. We give the syntax for two type theories, one with grades (the annotated language) and one without (the plain language). We prove some metatheoretic properties, and describe the semantics in terms of category theory. We show that the input signals to a quantum chip forms a model of the annotated language. We also give a syntatic model, prove that it is initial, and hence prove soundness and completeness theorems.