Proofs in the Nuprl system, an implementation of a constructive
type theory, yield “correct-by-construction” programs.
In this paper a new methodology is presented for
extracting efficient and readable programs from inductive
proofs. The resulting extracted programs are in a form suitable
for use in hierarchical verifications in that they are
amenable to clean partial evaluation via extensions to the
Nuprl rewrite system. The method is based on two elements:
specifications written with careful use of the Nuprl set-type
to restrict the extracts to strictly computational content; and
on proofs that use induction tactics that generate extracts using
familiar fixed-point combinators of the untyped lambda
calculus. In this paper the methodology is described and its
application is illustrated by example.