Skip to main content
PRL Project

Constructive Proofs and Program Extraction

by Christoph Kreitz

The purpose of this lecture is to demonstrate the computational aspects of Type Theory. I will briefly discuss the key features of the Nuprl Proof Development System and then present two different formal proofs of a theorem stating the existence of integer square roots. From a "classical" point of view, these two proofs lead to the same result, but computationally there are vast differences between them. I will demonstrate the latter by running the algorithms extracted from the proofs in the Nuprl system.

Background Literature:

Derivation of a Fast Integer Square Root Algorithm


[PS] [PDF]