2026-07-30T14:29:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27023 2026-07-30T09:16:25Z ddc:004 open_access

A Graded Modal Type Theory for Pulse Schedules Adams, Robin Bernardy, Jean-Philippe Perticone, Lorenzo Pope, Jeremy Quantum computing superconducting qubits linear type theory graded modal type theory 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₁ will represent a state of qubit Q₁ that will exist 50 nanoseconds in the future, and a variable y :^{-75} Q₂ will represent a state of qubit Q₂ 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 syntactic model, prove that it is initial, and hence prove soundness and completeness theorems. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robin Adams and Jean-Philippe Bernardy and Lorenzo Perticone and Jeremy Pope 2026 Is Part Of LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2025.5 urn:nbn:de:0030-drops-270237 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.5 eng https://creativecommons.org/licenses/by/4.0/legalcode