Welcome to the Nuprl in Coq webpage

This page contains information regarding our project of formalizing Nuprl in Coq.

---

Towards a Formally Verified Proof Assistant (ITP 2014)

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 omitted. 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:

• 2015-04-01
  • 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.
• 2015-04-30
  • We've proved a bar induction rule for free choice sequences of natural numbers (see bar_induction3.v and this paper)
  • We've proved many more rules related to exceptions (see rules_exception.v and rules_exception2.v).
• 2015-08-07
  • We've proved another bar induction rule for free choice sequences of closed terms without names (see bar_induction_cterm2.v).
  • Sources are now also available on github.