Abstract:

Correct Code-Generation in a Generic Framework

T. Meyer and Burkhart Wolff


One major motivation for theorem provers is the development of verified programs. In particular, synthesis or 
transformational development techniques aim at a formalised conversion of the original specification to a final 
formula meeting some notion of executability. We present a framework to describe such notions, a method to 
formally investigate them and instantiate it for three executable languages, based on three different forms of 
recursion (two denotational and one based on well-founded recursion) and develop their theory in Isabelle/HOL. 
These theories serve as a semantic interface for a generic code-generator which is set up for each program notion 
with an individual code-scheme for SML.