An Implementation of Homotopy Type Theory in Isabelle/Pure
Logic in Computer Science
2019-11-04 v1 Logic
Abstract
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 description of the underlying theory of the Isabelle/Pure logical framework, and discuss various issues and design decisions that arise when attempting to encode intensional dependent type theory with universes inside a simple type-theoretic logical foundation.
Keywords
Cite
@article{arxiv.1911.00399,
title = {An Implementation of Homotopy Type Theory in Isabelle/Pure},
author = {Joshua Chen},
journal= {arXiv preprint arXiv:1911.00399},
year = {2019}
}
Comments
Masters thesis