Name
Abstract | ||
|---|---|---|
This papers extends the Nuprl proof assistant (a system representative of the class of extensional type theories a la Martin-Lof) 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 meta-theoretical 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.
|
Year | DOI | Venue |
|---|---|---|
2016 | 10.1145/2854065.2854077 | CPP 2016: Certified Proofs and Programs
St. Petersburg
FL
USA
January, 2016 |
Keywords | DocType | ISBN |
Intuitionistic Type Theory, Nuprl, Coq, Continuity, Nominal Type Theory, Exceptions, Squashing, Truncation | Conference | 978-1-4503-4127-1 |
Citations | PageRank | References |
6 | 0.49 | 45 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vincent Rahli | 1 | 43 | 9.21 |
| M. Bickford | 2 | 101 | 8.60 |