# 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.*