Programs, Proofs and Parametrized Specifications

In a series of papers we have been using a modification of the ideas of Curry and Howard to obtain reliable programs from formal proofs. In this paper we extend our earlier work by presenting a new approach for constructing correct SML structures and SML functors from CASL structured and parametrized specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized specifications and then a program extraction procedure which produces SML programs that meet their specifications.