Homotopy Type Theory in Isabelle

DOI10.4230/LIPICS.ITP.2021.12MaRDI QIDQ6157254zbMATH OpenOpenAlexFDO

Authors Joshua Chen

Publication date 20 June 2023

Full work available at URL https://arxiv.org/abs/2002.09282

zbMATH Keywords

dependent type theoryhomotopy type theorylogical frameworksproof assistants

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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.

Cited in

(3)

• Homotopy Type Theory
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Modalities in homotopy type theory

This page was built for publication: Homotopy Type Theory in Isabelle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6157254)