Writing Constructive Proofs Yielding Efficient Extracted Programs
by Aleksey Nogin
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.
bibTex ref: Nog00