Welcome to the Nuprl in Coq webpageThis page contains information regarding our project of formalizing Nuprl in Coq.
Here is some complementary information regarding our ITP 2014 titled Towards a Formally Verified Proof Assistant:
- Our Technical Report is probably the best place to start. It is organized into chapters and has a structure similar to the paper. It provides more details for each part. The hyperlinked table of contents and Sec. 1.4 might be useful in directly getting to the right place.
- The above report shows key definitions
and many statements that we proved. Coq proof scripts are always
However, it has lines of the form:
---- begin file filename.v ----
which mark the start of key contents of our Coq source file filename.v . The filename is hyperlinked and points to a page that shows the entire contents of that file.
- Tarball containing all sources.
- A web-interface which can be used to lookup our Coq definitions by name.
Latest version of our implementation
This section contains, among other things, the supporting files for our papers titled:
Bar Induction: The Good, the Bad, and the Ugly (a long version with appendices is also available here)
Accepted to LICS 2017.
A Nominal Exploration of Intuitionism (a long version with appendices is also available here)
Presented at CPP 2016.
Coq as a Metatheory for Nuprl with Bar Induction
Presented at CCC 2015.
Since our ITP 2014 paper, we've extended our implementation in several ways.
Since August 2015, the Coq source files are now available on github. Instructions on how to compile our implementation are in the README file. It compiles using Coq 8.4pl6.
Here is a list of things we've added since our ITP 2014 paper:
- We've added library support for abstractions only.
- We've added names, named exceptions, exception handlers, and a fresh operator to generate fresh names.
- Using these nominal features, we've proved a version of Brouwer's Continuity Principle for numbers. See continuity_roadmap.v for a roadmap.