Writing Constructive Proofs Yielding Efficient Extracted Programs

unofficial copies [PDF], [PS]


by Aleksey Nogin

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

Abstract

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.