# * Writing Constructive Proofs Yielding Efficient Extracted Programs *

## by Aleksey Nogin

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.

**bibTex ref: Nog00**

cite link