Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
Mark has formalized in Nuprl much of Chapter Two of Bishop's book on constructive real analysis using a more efficient representation of the reals so that it is feasible to compute with these infinite precision real numbers. This seminar will be an elementary presentation of the basic ideas with examples of interesting computations on the reals that take advantage of unique features of the Nuprl constructive type theory.
Bob will give a brief ten minute history of this effort by Bishop and its influence on the creation of constructive type theory. Bishop's visit to Cornell was a significant influence on the design of Nuprl which captured elements of Bishop's pragmatic philosophy as well as of his elegant mathematics. His book on analysis has become a well known classic.
Date: April 10, 2014
Location: Gates 122