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...     »

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...     »