Document Open Access Logo

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities

Authors Carlo Angiuli , Kuen-Bang Hou (Favonia) , Robert Harper

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.6.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Carlo Angiuli
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Kuen-Bang Hou (Favonia)
  • School of Mathematics, Institute for Advanced Study, Princeton, NJ, USA
Robert Harper
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This research was supported by the Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053 and the National Science Foundation through grant DMS-1638352. Any opinions, findings and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of any sponsoring institution, the U.S. government or any other entity.
  • Hou (Favonia), Kuen-Bang: This author thanks the Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program "Big Proof" when part of work on this paper was undertaken. The program was supported by EPSRC grant number EP/K032208/1.

Cite As Get BibTex

Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.6

Abstract

We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Homotopy Type Theory
  • Two-Level Type Theory
  • Computational Type Theory
  • Cubical Sets

Metrics

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

Related Versions

References

  1. Stuart F. Allen. A Non-type-theoretic Definition of Martin-Löf’s Types. In D. Gries, editor, Proceedings of the 2nd IEEE Symposium on Logic in Computer Science, pages 215-224, Ithaca, NY, 1987. IEEE Computer Society Press. Google Scholar
  2. Stuart F Allen, Mark Bickford, Robert L Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran. Innovations in computational type theory using Nuprl. Journal of Applied Logic, 4(4):428-469, 2006. Google Scholar
  3. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), pages 21:1-21:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2016.21.
  4. Abhishek Anand and Vincent Rahli. Towards a formally verified proof assistant. In Interactive Theorem Proving, pages 27-44, Cham, 2014. Springer International Publishing. Google Scholar
  5. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. Cartesian cubical type theory. Preprint, December 2017. URL: https://github.com/dlicata335/cart-cube.
  6. Carlo Angiuli, Robert Harper, and Todd Wilson. Computational higher-dimensional type theory. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 680-693, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3009837.3009861.
  7. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Computational higher type theory III: Univalent universes and exact equality, December 2017. URL: http://arxiv.org/abs/1712.01800.
  8. Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. Two-level type theory and applications, 2017. URL: http://arxiv.org/abs/1705.03307.
  9. Steve Awodey. A cubical model of homotopy type theory, June 2016. URL: https://www.andrew.cmu.edu/user/awodey/preprints/stockholm.pdf.
  10. Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1):45-55, 2009. URL: http://dx.doi.org/10.1017/S0305004108001783.
  11. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT library: A formalization of homotopy type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 164-172, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3018610.3018615.
  12. Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26, pages 107-128, Toulouse, France, 2014. Dagstuhl Publishing. Google Scholar
  13. Marc Bezem, Thierry Coquand, and Simon Huber. The univalence axiom in cubical sets, October 2017. URL: http://arxiv.org/abs/1710.10941.
  14. Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy type theory in Agda, 2018. URL: https://github.com/HoTT/HoTT-Agda.
  15. Ulrik Buchholtz and Edward Morehouse. Varieties of cubical sets. In Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings, pages 77-92. Springer International Publishing, Cham, 2017. URL: http://dx.doi.org/10.1007/978-3-319-57418-9_5.
  16. Evan Cavallo and Robert Harper. Computational higher type theory IV: Inductive types, January 2018. URL: http://arxiv.org/abs/1801.01568.
  17. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69, 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.
  18. Thierry Coquand. Variations on cubical sets, 2014. URL: http://www.cse.chalmers.se/~coquand/diag.pdf.
  19. Simon Huber. Cubical Interpretations of Type Theory. PhD thesis, University of Gothenburg, 2016. Google Scholar
  20. Chris Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky), June 2016. URL: http://arxiv.org/abs/1211.2851.
  21. Daniel R. Licata. Weak univalence with "beta" implies full univalence. Email to the Homotopy Type Theory mailing list, 2016. URL: https://groups.google.com/forum/#!topic/homotopytypetheory/j2KBIvDw53s.
  22. Daniel R. Licata and Guillaume Brunerie. A cubical type theory, November 2014. Talk at Oxford Homotopy Type Theory Workshop. URL: http://dlicata.web.wesleyan.edu/pubs/lb14cubical/lb14cubes-oxford.pdf.
  23. Peter LeFanu Lumsdaine and Mike Shulman. Semantics of higher inductive types, May 2017. URL: http://arxiv.org/abs/1705.07088.
  24. P. Martin-Löf. Constructive mathematics and computer programming. Philosophical Transactions of the Royal Society of London Series A, 312:501-518, 1984. URL: http://dx.doi.org/10.1098/rsta.1984.0073.
  25. Per Martin-Löf. Intuitionistic type theory. Bibliopolis, Naples, Italy, 1984. Google Scholar
  26. A. M. Pitts. Nominal presentation of cubical sets models of type theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014), pages 202-220, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2014.202.
  27. W. W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198-212, 1967. URL: http://dx.doi.org/10.2307/2271658.
  28. The RedPRL Development Team. RedPRL - the People’s Refinement Logic, 2018. URL: http://www.redprl.org/.
  29. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  30. Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. Homotopy type theory in Lean. In Interactive Theorem Proving, pages 479-495, Cham, 2017. Springer. URL: http://dx.doi.org/10.1007/978-3-319-66107-0_30.
  31. Vladimir Voevodsky. The equivalence axiom and univalent models of type theory, 2010. Notes from a talk at Carnegie Mellon University. URL: http://www.math.ias.edu/vladimir/files/CMU_talk.pdf.
  32. Vladimir Voevodsky. Univalent foundations project. Modified version of an NSF grant application, October 2010. URL: http://www.math.ias.edu/vladimir/files/univalent_foundations_project.pdf.
  33. Vladimir Voevodsky. A type system with two kinds of identity types. Slides available at https://uf-ias-2012.wikispaces.com/file/view/HTS_slides.pdf/410105196/HTS_slides.pdf, 2013. URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf.
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