Search Results

Documents authored by Adams, Robin

Artifact
Software
DOI: 10.4230/artifacts.27329
Graded Modal Type Theory for Pulse Schedules

Authors: Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, and Jeremy Pope

Abstract
Cite as

Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, Jeremy Pope. Graded Modal Type Theory for Pulse Schedules (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27329,
   title = {{Graded Modal Type Theory for Pulse Schedules}}, 
   author = {Adams, Robin and Bernardy, Jean-Philippe and Perticone, Lorenzo and Pope, Jeremy},
   note = {Software, This research was funded by the SSF (Swedish Foundation for Strategic Research) project QuantumStack, grant number FUS21-0063., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:bc79e493a8f11d72e5382289e1ef8d1284024082;origin=https://codeberg.org/radams78/grampus.git;visit=swh:1:snp:dfc2042f8a825085f51d25ac29729c9fbbe428d6;anchor=swh:1:rev:71bd1fc1fe6105e27027da7b208cf83da35f9b4f}{\texttt{swh:1:dir:bc79e493a8f11d72e5382289e1ef8d1284024082}} (visited on 2026-07-30)},
   url = {https://codeberg.org/radams78/grampus.git},
   doi = {10.4230/artifacts.27329},
}
Document
DOI: 10.4230/LIPIcs.TYPES.2025.5
A Graded Modal Type Theory for Pulse Schedules

Authors: Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, and Jeremy Pope

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract
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.
Cite as

Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, and Jeremy Pope. A Graded Modal Type Theory for Pulse Schedules. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{adams_et_al:LIPIcs.TYPES.2025.5,
  author =	{Adams, Robin and Bernardy, Jean-Philippe and Perticone, Lorenzo and Pope, Jeremy},
  title =	{{A Graded Modal Type Theory for Pulse Schedules}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.5},
  URN =		{urn:nbn:de:0030-drops-270237},
  doi =		{10.4230/LIPIcs.TYPES.2025.5},
  annote =	{Keywords: Quantum computing, superconducting qubits, linear type theory, graded modal type theory}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2016.3
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic

Authors: Robin Adams, Marc Bezem, and Thierry Coquand

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property of canonicity - that every closed term computes to a canonical form. A computation becomes "stuck" when it reaches the point that it needs to evaluate a proof term that is an application of the univalence axiom. So we wish to find a way to compute with the univalence axiom. While this problem has been solved with the formulation of cubical type theory, where the computations are expressed using a nominal extension of lambda-calculus, it may be interesting to explore alternative solutions, which do not require such an extension. As a first step, we present here a system of propositional higher-order minimal logic (PHOML). There are three kinds of typing judgement in PHOML. There are terms which inhabit types, which are the simple types over Omega. There are proofs which inhabit propositions, which are the terms of type Omega. The canonical propositions are those constructed from false by implication. Thirdly, there are paths which inhabit equations M =_A N, where M and N are terms of type A. There are two ways to prove an equality: reflexivity, and propositional extensionality - logically equivalent propositions are equal. This system allows for some definitional equalities that are not present in cubical type theory, namely that transport along the trivial path is identity. We present a call-by-name reduction relation for this system, and prove that the system satisfies canonicity: every closed typable term head-reduces to a canonical form. This work has been formalised in Agda.
Cite as

Robin Adams, Marc Bezem, and Thierry Coquand. A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{adams_et_al:LIPIcs.TYPES.2016.3,
  author =	{Adams, Robin and Bezem, Marc and Coquand, Thierry},
  title =	{{A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{3:1--3:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.3},
  URN =		{urn:nbn:de:0030-drops-98581},
  doi =		{10.4230/LIPIcs.TYPES.2016.3},
  annote =	{Keywords: type theory, univalence, canonicity}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2015.1
A Type Theory for Probabilistic and Bayesian Reasoning

Authors: Robin Adams and Bart Jacobs

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract
This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.
Cite as

Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 1:1-1:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{adams_et_al:LIPIcs.TYPES.2015.1,
  author =	{Adams, Robin and Jacobs, Bart},
  title =	{{A Type Theory for Probabilistic and Bayesian Reasoning}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{1:1--1:34},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.1},
  URN =		{urn:nbn:de:0030-drops-84714},
  doi =		{10.4230/LIPIcs.TYPES.2015.1},
  annote =	{Keywords: Probabilistic programming, probabilistic algorithm, type theory, effect module, Bayesian reasoning}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact