CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
Tue 19 Jan 2016 11:30 - 12:00 at Room St Petersburg II - Session 6: Foundations

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.

Tue 19 Jan

CPP-2016-main
10:30 - 12:00: CPP - Session 6: Foundations at Room St Petersburg II
CPP-2016-main10:30 - 11:00
Talk
Nathan FultonCarnegie Mellon University, André Platzer
CPP-2016-main11:00 - 11:30
Talk
Floris van DoornCarnegie Mellon University
CPP-2016-main11:30 - 12:00
Talk
Vincent RahliSnT, Mark BickfordCornell University