The ability to extract ``correct-by-construction'' programs directly from proofs is the most notable feature of constructive type theories as implemented in Nuprl [6] and related systems [21,8,24]. As Howe demonstrated , it is possible to use these methods even with classically proved equations from HOL. Since the LPE will widen the applicability of this methodology, we propose to improve its practical effectiveness.
Despite substantial experience with this extraction methodology since 1984 when we introduced it, there still is no established software engineering practice based on the extraction of programs from constructive proofs. We have an opportunity to improve the technology for this as we build the LPE since it will include the Nuprl logic engine and extractor.
A key obstacle to the transition of program extraction methods into practice is the lack of a methodology for extracting clear and readable programs from formal proofs. Often, the extracted programs contain unnecessary structure, artifacts of the constructive proof, that do not contribute to the computational content of the extracted term. Researchers have addressed this problem in various constructive systems in an attempt to improve the efficiency, readability, and understanding of extracted programs [26,16,27].
Nuprl is unique among the existing systems in it's ability to formalize and verify induction principles as lemmas within the type theory that yield extracts that are recursion schemes optimized for both readability and efficiency.
The proposed investigation under this item is the development of libraries of induction principles having efficient recursion schemes as their extracts. This extends work in [4].