Skip to main content
PRL Project

Writing Constructive Proofs Yielding Efficient Extracted Programs

by Aleksey Nogin

  • unofficial copies PDF, PS

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

cite link