Moving Proofs-As-Programs into Practice

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.

• Type: Conference
• Year: 1997
• Where: KBSE
• Authors: James L. Caldwell
• Keywords: KBSE 1997, Nuprl, Nuprl Rewrite System, Nuprl System, Software Engineering