2 papers
cs.LO2020
Homotopy Type Theory in Isabelle
Joshua Chen
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 l…
cs.LO2019
An Implementation of Homotopy Type Theory in Isabelle/Pure
Joshua Chen
In this Masters thesis we present an implementation of a fragment of "book HoTT" as an object logic for the interactive proof assistant Isabelle. We also give a mathematical descri…