Abstract

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

http://www.nuprl.org/Algorithms/03cucs-intsqrt.pdf

http://www.nuprl.org/Algorithms/03cucs-intsqrt.ps

Slides:

[PS] [PDF]