Back to my publicationsThe NuPRL system was designed for interactive writing of machine-checked constructive proofs and for extracting algorithms from the proofs. The extracted algorithms are guaranteed to be correct which makes it possible to use NuPRL as a programming language with built-in verification. However it turned out that proofs written without algorithmic efficiency in mind often produce very inefficient algorithms -- exponential and double-exponential ones for problems that can be solved in polynomial time.
In this paper we present some general principles of efficient programming in constructive type theory as well as describe a case study that shows how these principles apply to particular problems. We consider the proof of the Myhill-Nerode automata minimization theorem from the NuPRL automata library which leaded to a double-exponential (in time) extracted program. Systematic use of the presented principles allowed us to build a new complexity cautious proof leading to polynomial-time algorithm extracted by the same NuPRL extractor.
Last update: Friday, March 18, 2005 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)