Formalizing Constructive Analysis in Nuprl

Many thanks to Springer and Bridges for permission to use their work here.

Constructive Analysis, written in 1985 by Errett Bishop and Douglas Bridges has been an insightful tool and inspiration to our work in Nuprl.

Mark Bickford has formalized Chapter Two of Constructive Analysis in Nuprl, creating detailed definitions and proofs.

Click on the book cover to find the text of chapter two where each highlighted portion is linked to its formalized Nuprl version.

A lecture detailing the formalization of Bishop's Constructive Analysis was given by Mark Bickford at the 2016 Interval Analysis and Constructive Mathematics Workshop in Oaxaca. A video of the lecture can be found here: Formalized Brouwerian Real Analysis using the Nuprl proof assistant.