User: Guest  Login
Original title:
Verified Code Generation from Isabelle/HOL 
Translated title:
Verifizierte Code-Generierung aus Isabelle/HOL 
Year:
2019 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.); Myreen, Magnus (Prof., Ph.D.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
TUM classification:
DAT 706d; DAT 540d 
Abstract:
In this thesis, I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation. The work consists of three major contributions: a certifying routine to eliminate type classes and instances, an algebra for higher-order Lambda-terms, and a compiler that works similarly to the existing code generator, but produces a CakeML abstract...    »
 
Translated abstract:
Diese Dissertation entwickelt ein verifizierte Compiler-Toolkette von ausführbaren Spezifikationen in Isabelle/HOL zu abstrakten Syntaxbäumen in CakeML. Dies verbessert den Stand der Technik in Isabelle, indem es eine vertrauenswürdige Prozedur für Codegenerierung bereitstellt. Die Arbeit besteht aus drei Hauptbeiträgen: einer zertifizierende Routine zur Eliminierung von Typklassen und Instanzen, einer Algebra für höherstufige Lambda-Terme und einem Compiler, der ähnlich wie der existierende Cod...    »
 
Oral examination:
11.07.2019 
File size:
3434482 bytes 
Pages:
149 
Last change:
30.07.2019