| Correct Code-Generation in a Generic Framework (2007) | |||||||||||||||
Abstract | |||||||||||||||
| . One major motivation for theorem provers is the development of veried programs. In particular, synthesis or transformational development techniques aim at a formalised conversion of the original specication to a nal 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 dierent 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. 1 Introduction This paper is concerned with the combination of specication notations and program notions, or more precisely, data-view oriented specication formalisms and functional programming languages. While many specication formalisms (such as B, KIV/VSE, but also COQ [3, 5, 2])... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||