Code generation denotes the translation of an abstract formal specification into a corresponding executable program. The aim of this thesis is to present a code generator framework for the interactive proof assistant Isabelle/HOL, an implementation of higher-order logic. It comes with two substantial novelties: a general but lightweight concept for datatype abstraction and support for Isabelle type classes in the manner of Haskell type classes. Code can be generated for functional programming languages supporting pattern matching, concrete instances for SML, OCaml and Haskell are presented.    «

Code generation denotes the translation of an abstract formal specification into a corresponding executable program. The aim of this thesis is to present a code generator framework for the interactive proof assistant Isabelle/HOL, an implementation of higher-order logic. It comes with two substantial novelties: a general but lightweight concept for datatype abstraction and support for Isabelle type classes in the manner of Haskell type classes. Code can be generated for functional programming...    »

Codegenerierung bezeichnet die automatische Überführung einer abstrakten formalen Spezifikation in ein korrespondierendes ausführbares Programm. Ziel dieser Arbeit ist die Darstellung eines Codegenerator-Frameworks für den interaktiven Theorembeweiser Isabelle/HOL, einer Implementierung höherstufiger Logik. Gegenüber existierenden Ansätzen weist das Framework zwei substantielle Neuerungen auf: ein sehr allgemeines, aber leichtgewichtiges Konzept für Datentypabstraktion und die Unterstützung von Isabelle-Typklassen im Sinne von Haskell-Typklassen. Konzeptionell möglich ist Generierung von Code für funktionale Sprachen mit Pattern Matching; konkrete Instantiierungen des Frameworks liegen vor für die Zielsprachen SML, OCaml und Haskell.     «

Codegenerierung bezeichnet die automatische Überführung einer abstrakten formalen Spezifikation in ein korrespondierendes ausführbares Programm. Ziel dieser Arbeit ist die Darstellung eines Codegenerator-Frameworks für den interaktiven Theorembeweiser Isabelle/HOL, einer Implementierung höherstufiger Logik. Gegenüber existierenden Ansätzen weist das Framework zwei substantielle Neuerungen auf: ein sehr allgemeines, aber leichtgewichtiges Konzept für Datentypabstraktion und die Unterstützung vo...    »