The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory

Authors Bassel Mannaa, Rasmus Ejlers Møgelberg



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.23.pdf
  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Author Details

Bassel Mannaa
  • Department of Computer Science, IT University of Copenhagen, Copenhagen, Denmark
Rasmus Ejlers Møgelberg
  • Department of Computer Science, IT University of Copenhagen, Copenhagen, Denmark

Cite AsGet BibTex

Bassel Mannaa and Rasmus Ejlers Møgelberg. The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.23

Abstract

Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of type checking. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types. The main challenge for constructing this model is to model the notion of ticks used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion, but in this category there is no object of ticks, so tick-assumptions in a context can not be modelled using standard tools. Instead we show how ticks can be modelled using adjoint functors, and how to model the tick constant using a semantic substitution.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
Keywords
  • Guarded type theory
  • Coinduction
  • Presheaf model
  • Clocked type theory
  • Dependent adjunction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. A. W. Appel and D. A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst, 23(5):657-683, 2001. Google Scholar
  2. R. Atkey and C. McBride. Productive coprogramming with guarded recursion. In ICFP, pages 197-208. ACM, 2013. Google Scholar
  3. P. Bahr, H. B. Grathwohl, and R. E. Møgelberg. The clocks are ticking: No more delays! In LICS, pages 1-12. IEEE, 2017. Google Scholar
  4. J.-P. Bernardy, T. Coquand, and G. Moulin. A presheaf model of parametric type theory. Electronic Notes in Theoretical Computer Science, 319:67-82, 2015. Google Scholar
  5. L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, and A. Vezzosi. Guarded cubical type theory: Path equality for guarded recursion. In CSL, 2016. Google Scholar
  6. L. Birkedal and R. E. Møgelberg. Intensional type theory with guarded recursive types qua fixed points on universes. In LICS, pages 213-222. IEEE, 2013. Google Scholar
  7. L. Birkedal, R.E. Møgelberg, J. Schwinghammer, and K. Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. LMCS, 8(4), 2012. Google Scholar
  8. A. Bizjak, L. Birkedal, and M. Miculan. A model of countable nondeterminism in guarded type theory. In RTA-TLCA, pages 108-123, 2014. Google Scholar
  9. A. Bizjak, H. B. Grathwohl, R. Clouston, R. E. Møgelberg, and L. Birkedal. Guarded dependent type theory with coinductive types. In FOSSACS, 2016. Google Scholar
  10. A. Bizjak and R. Møgelberg. Denotational semantics for guarded dependent type theory. arXiv, 2017. URL: http://arxiv.org/abs/1802.03744.
  11. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2015.5.
  12. T. Coquand. Infinite objects in type theory. In International Workshop on Types for Proofs and Programs, pages 62-78. Springer, 1993. Google Scholar
  13. P. Dybjer. Internal type theory. In International Workshop on Types for Proofs and Programs, pages 120-134. Springer, 1995. Google Scholar
  14. P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984. Google Scholar
  15. C. McBride and R. Paterson. Applicative programming with effects. Journal of functional programming, 18(1):1-13, 2008. Google Scholar
  16. H. Nakano. A modality for recursion. In LICS, pages 255-266, 2000. Google Scholar
  17. A. M. Pitts, J. Matthiesen, and J. Derikx. A dependent type theory with abstractable names. Electronic Notes in Theoretical Computer Science, 312:19-50, 2015. Google Scholar
  18. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail