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 syntax tree together with a correctness theorem.
«
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 Codegenerator funktioniert, jedoch abstrakte CakeML-Syntax zusammen mit einem Korrektheitstheorem erzeugt.
«
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...
»