Showing cs.LOShow all
3 papers · 1 filter
cs.LO2025
2-Coherent Internal Models of Homotopical Type Theory
Joshua Chen
The program of internal type theory seeks to develop the categorical model theory of dependent type theory using the language of dependent type theory itself. In the present work w…
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…