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.
Derivation of a Fast Integer Square Root Algorithm