KnowledgeBase » SEMINAR » ID = 727

Formalizing Bishop's Constructive Analysis in Constructive Type Theory

by Mark Bickford, Robert L. Constable
2014

Abstract

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
Time: 2:45-3:45pm
Location: Gates 122