diff options
| author | Josh Chen | 2019-10-29 11:51:26 +0100 |
|---|---|---|
| committer | GitHub | 2019-10-29 11:51:26 +0100 |
| commit | 32dc5b962b171a180568c1352a4a3301029605a1 (patch) | |
| tree | 782e4681dccd49fecb4bc74848e9f9db869f3f47 | |
| parent | b815a897c04350f6b2335a15e30844316a5cce9e (diff) | |
Update README.md
| -rw-r--r-- | README.md | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -2,6 +2,9 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory) in [Isabelle](https://isabelle.in.tum.de/). +**Update [15 Oct 2019]**: +Convenience and readability of formalizations in the library is taking a hit as we move to the limits of the currently available functionality in Isabelle, so for the moment development has moved [here](https://github.com/jaycech3n/Isabelle-Spartan), in order to first build more necessary automation and improve the framework. + ### Usage The default entry point for the logic is `HoTT`, import this to load everything else. @@ -16,7 +19,8 @@ In its current state it is best viewed as a formalization of HoTT within Isabell Work is slowly ongoing to develop the logic into a fully-featured framework in which one can formulate and prove mathematical statements, in the style of the univalent foundations school. While Isabelle has provided support for object logics based on Martin-Löf type theory since the beginning, these have largely been ignored in favor of Isabelle/HOL. Thus this project is also an experiment in creating a viable framework, based on dependent type theory, inside the simple type theoretic foundations of Isabelle/Pure. -**Update (15 Oct 2019)**: Framework development currently [here](https://github.com/jaycech3n/Isabelle-Spartan). + +A writeup of some theoretical considerations in this implementation is in my [Masters thesis](https://joshchen.io/assets/ms_thesis_submitted.pdf). ### License |