Abstract
This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories `a la Martin-Löf) with named exceptions and handlers, as well as a nominal fresh operator. Using these new features, we prove a version of Brouwer’s Continuity Principle for numbers. We also provide a simpler proof of a weaker version of this principle that only uses diverging terms. We prove these two principles in Nuprl’s meta-theory using our formalization of Nuprl in Coq and show how we can reflect these metatheoretical results in the Nuprl theory as derivation rules. We also show that these additions preserve Nuprl’s key meta-theoretical properties, in particular consistency and the congruence of Howe’s
computational equivalence relation. Using continuity and the fan theorem we prove important results of Intuitionistic Mathematics: Brouwer’s continuity theorem and bar induction on monotone bars.
computational equivalence relation. Using continuity and the fan theorem we prove important results of Intuitionistic Mathematics: Brouwer’s continuity theorem and bar induction on monotone bars.
Original language | English |
---|---|
Title of host publication | Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016 |
Publisher | Association for Computing Machinery (ACM) |
Pages | 130-141 |
Number of pages | 12 |
ISBN (Electronic) | 9781450341271 |
DOIs | |
Publication status | Published - 18 Jan 2016 |
Event | 5th ACM SIGPLAN Conference on Certified Programs and Proofs - St. Petersburg, FL, United States Duration: 18 Jan 2016 → 19 Jan 2016 |
Conference
Conference | 5th ACM SIGPLAN Conference on Certified Programs and Proofs |
---|---|
Country/Territory | United States |
City | St. Petersburg, FL |
Period | 18/01/16 → 19/01/16 |
Keywords
- Intuitionistic Type Theory
- Nuprl
- Coq
- Continuity
- Nominal Type Theory
- Exceptions
- Squashing
- Truncation