Writing Constructive Proofs Yielding Efficient Extracted Programs

unofficial copies [PDF], [PS]

by Aleksey Nogin

Electronic Notes in Theoretical Computer Science, vol. 37, 2001.


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 extractor. We believe that the principles presented in this paper in combination with other methods may lead to an efficient technique of programming-by-proofs.