Document Open Access Logo

Homotopy Type Theory in Isabelle

Author Joshua Chen

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.12.pdf
  • Filesize: 0.65 MB
  • 8 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Theory of computation → Higher order logic
Keywords
  • Proof assistants
  • Logical frameworks
  • Dependent type theory
  • Homotopy type theory

Metrics

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

Abstract

This paper introduces Isabelle/HoTT, the first development of homotopy type theory in the Isabelle proof assistant. Building on earlier work by Paulson, I use Isabelle’s existing logical framework infrastructure to implement essential automation, such as type checking and term elaboration, that is usually handled on the source code level of dependently typed systems. I also integrate the propositions-as-types paradigm with the declarative Isar proof language, providing an alternative to the tactic-based proofs of Coq and the proof terms of Agda. The infrastructure developed is then used to formalize foundational results from the Homotopy Type Theory book.

Cite As Get BibTex

Joshua Chen. Homotopy Type Theory in Isabelle. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 12:1-12:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.12

Author Details

Joshua Chen
  • University of Nottingham, UK

Funding

Partially funded by ERC project SMART (starting grant no. 714034) and the Royal Society (grant URF\R1\191055).

Supplementary Materials

References

  1. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending Homotopy Type Theory with Strict Equality. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.21.
  2. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. In Dan Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), volume 119 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.6.
  3. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications, 2019. URL: http://arxiv.org/abs/1705.03307.
  4. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a logical framework based on the λπ-calculus modulo theory, 2016. URL: http://www.lsv.fr/~dowek/Publi/expressing.pdf.
  5. Bruno Barras and Valentin Maestracci. Implementation of two layers type theory in Dedukti and application to cubical type theory. Electronic Proceedings in Theoretical Computer Science, 332:54–67, January 2021. URL: https://doi.org/10.4204/eptcs.332.4.
  6. 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, page 164–172, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3018610.3018615.
  7. Guillaume Brunerie, Kuen-Bang Hou (Favonia), Evan Cavallo, Tim Baumann, Eric Finster, Jesper Cockx, Christian Sattler, Chris Jeris, Michael Shulman, et al. Homotopy type theory in Agda, 2021. URL: https://github.com/HoTT/HoTT-Agda.
  8. 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: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  9. Jana Dunfield and Neel Krishnaswami. Bidirectional typing, 2020. URL: http://arxiv.org/abs/1908.05839.
  10. Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science, 25(5):1116–1131, 2015. URL: https://doi.org/10.1017/S0960129514000528.
  11. Bart Jacobs and Thomas F. Melham. Translating dependent type theory into higher order logic. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA '93, page 209–229, Berlin, Heidelberg, 1993. Springer-Verlag. Google Scholar
  12. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/tutorial.pdf.
  13. Lawrence C. Paulson. Constructive Type Theory, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/logics.pdf.
  14. The Univalent Foundations Program and Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, 1st edition, 2013.
  15. University of Cambridge, Technische Universität München, and Contributors. Isabelle2020, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020.
  16. Vladimir Voevodsky. A simple type system with two identity types, February 2013. Unpublished note, available online at https://www.math.ias.edu/vladimir/Lectures. URL: https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf.
  17. Makarius Wenzel. The Isabelle/Isar Reference Manual, April 2020. URL: https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/isar-ref.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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact