User: Guest  Login
Original title:
Code Generation from Specifications in Higher-Order Logic 
Translated title:
Codegenerierung aus Spezifikationen in höherstufiger Logik 
Year:
2009 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Seidl, Helmut (Prof. Dr.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
theorem proving, code generation, higher-order logics 
Translated keywords:
Theorembeweiser, Codegenerierung, höherstufige Logik 
Abstract:
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...    »
 
Translated abstract:
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...    »
 
Oral examination:
08.12.2009 
Pages:
139 
Last change:
04.02.2010