Benutzer: Gast  Login
Originaltitel:
Code Generation from Specifications in Higher-Order Logic 
Übersetzter Titel:
Codegenerierung aus Spezifikationen in höherstufiger Logik 
Jahr:
2009 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Seidl, Helmut (Prof. Dr.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
theorem proving, code generation, higher-order logics 
Übersetzte Stichworte:
Theorembeweiser, Codegenerierung, höherstufige Logik 
Kurzfassung:
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...    »
 
Übersetzte Kurzfassung:
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...    »
 
Mündliche Prüfung:
08.12.2009 
Seiten:
139 
Letzte Änderung:
04.02.2010