The Constructive Real Numbers

Dr. Mark Bickford will discuss his implementation of the constructive reals in Nuprl, and we will discuss their significance both in practical applications and in the development of type theory. Supplementary material for this lecture is written by Dr. Bickford and included on the course web page for Lectures 16 and 17. He will also discuss his very insightful new result about the connectedness of the reals.