KnowledgeBase » 
SEMINAR
» ID = 610
Constructive Proofs and Program Extraction
by Christoph Kreitz
2003-2004
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: