tchajed/goedel-t
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
Formalization of termination of Gödel's System T
91 commits 1 branch 0 tags 112 KiB
  • Rocq Prover 99.1%
  • Makefile 0.9%
Find a file
Exact
Tej Chajed 03dcdc9f29
 Use strict bulleting throughout
2021-06-06 11:12:46 -04:00
.github/workflows Fix one of the issues with Coq master 2021-06-06 08:37:45 -04:00
.gitignore Updates for Coq 8.13+alpha 2020-08-29 19:16:23 -05:00
_CoqProject Fix one of the issues with Coq master 2021-06-06 08:37:45 -04:00
Examples.v Use strict bulleting for example execution 2021-06-06 11:08:35 -04:00
Extraction.v Add extraction of evaluator 2016-07-06 15:14:20 -04:00
Makefile Add an example program 2016-09-22 11:13:00 -04:00
README.md Switch from Travis to GitHub Actions 2021-06-06 08:15:35 -04:00
Reflect.v Add build system and separate out [expr_denote] 2016-07-06 15:12:37 -04:00
stlc.v type safety for stlc 2016-06-29 19:35:29 -07:00
SystemT.v Use strict bulleting throughout 2021-06-06 11:12:46 -04:00

README.md

Totality of Gödel's System T

CI

Formalization of Tait's proof of the totality of Gödel's System T using logical relations and hereditary termination in Coq.

Based on development presented by Bob Harper at OPLSS 2016.