Program development through proof transformation
Frank Pfenning · Contemporary mathematics - American Mathematical Society · 1990
We present a methodology for deriving verified programs that combines theorem proving and proof transformation steps. It extends the paradigm employed in systems like NuPrl where a program is developed and verified through the proof of the specification in a constructive type theory. We illustrate our methodology through an extended example -- a derivation of Warshall's algorithm for graph reachability. We also outline how our framework supports the definition, implementation, and use of abstract data types.