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