Document Open Access Logo

Guarded Cubical Type Theory: Path Equality for Guarded Recursion

Authors Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi

PDF
Thumbnail PDF

File

LIPIcs.CSL.2016.23.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Author Details

Lars Birkedal
Aleš Bizjak
Ranald Clouston
Hans Bugge Grathwohl
Bas Spitters
Andrea Vezzosi

Cite As Get BibTex

Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CSL.2016.23

Abstract

This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.

Subject Classification

Keywords
  • Guarded Recursion
  • Dependent Type Theory
  • Cubical Type Theory
  • Denotational Semantics
  • Homotopy Type Theory

Metrics

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

References

  1. Andreas Abel and Andrea Vezzosi. A formalized proof of strong normalization for guarded recursive types. In APLAS, pages 140-158, 2014. Google Scholar
  2. Thorsten Altenkirch, Conor McBride, and Wouter Swierstra. Observational equality, now! In PLPV, pages 57-68, 2007. Google Scholar
  3. Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. In ICFP, pages 197-208, 2013. Google Scholar
  4. Lars Birkedal and Rasmus Ejlers Møgelberg. Intensional type theory with guarded recursive types qua fixed points on universes. In LICS, pages 213-222, 2013. Google Scholar
  5. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. LMCS, 8(4), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(4:1)2012.
  6. Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, and Hongseok Yang. Step-indexed Kripke models over recursive worlds. In POPL, pages 119-132, 2011. Google Scholar
  7. Aleš Bizjak and Rasmus Ejlers Møgelberg. A model of guarded recursion with clock synchronisation. In MFPS, pages 83-101, 2015. Google Scholar
  8. Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, and Lars Birkedal. Guarded dependent type theory with coinductive types. In FoSSaCS, pages 20-35, 2016. Google Scholar
  9. Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. Programming and reasoning with guarded recursion for coinductive types. In FoSSaCS, pages 407-421, 2015. Google Scholar
  10. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. Unpublished, 2016. Google Scholar
  11. Thierry Coquand. Internal version of the uniform Kan filling condition. Unpublished, 2015. URL: http://www.cse.chalmers.se/~coquand/shape.pdf.
  12. Peter Dybjer. Internal type theory. In TYPES'95, pages 120-134, 1996. Google Scholar
  13. Martin Hofmann. Extensional constructs in intensional type theory. Springer, 1997. Google Scholar
  14. Martin Hofmann and Thomas Streicher. Lifting Grothendieck universes. Unpublished, 1999. URL: http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
  15. Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. The simplicial model of univalent foundations. arXiv:1211.2851, 2012. Google Scholar
  16. Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic. Springer, 1992. URL: http://dx.doi.org/10.1007/978-1-4612-0927-0.
  17. Per Martin-Löf. An intuitionistic theory of types: predicative part. In Logic Colloquium 1973, pages 73-118, 1975. Google Scholar
  18. The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0. URL: http://coq.inria.fr.
  19. Conor McBride and Ross Paterson. Applicative programming with effects. J. Funct. Programming, 18(1):1-13, 2008. Google Scholar
  20. Rasmus Ejlers Møgelberg. A type theory for productive coprogramming via guarded recursion. In CSL-LICS, 2014. Google Scholar
  21. Hiroshi Nakano. A modality for recursion. In LICS, pages 255-266, 2000. Google Scholar
  22. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  23. Ian Orton and Andrew M. Pitts. Axioms for modelling cubical type theory in a topos. In CSL, 2016. Google Scholar
  24. Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report ECS-LFCS-92-208, LFCS, University of Edinburgh, 1992. Google Scholar
  25. Bas Spitters. Cubical sets as a classifying topos. TYPES, 2015. Google Scholar
  26. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact