Tactic-Based Optimized Compilation of Functional Programs

14 years 22 days ago
Tactic-Based Optimized Compilation of Functional Programs
Abstract Within a framework of correct code-generation from HOLspecifications, we present a particular instance concerned with the optimized compilation of a lazy language (called MiniHaskell) to a strict language (called MiniML). Both languages are defined as shallow embeddings into denotational semantics based on Scott’s cpo’s, leading to a derivation of the corresponding operational semantics in order to cross-check the basic definitions. On this basis, translation rules from one language to the other were formally derived in Isabelle/HOL. Particular emphasis is put on the optimized compilation of function applications leading to the side-calculi inferring e.g. strictness of functions. The derived rules were grouped and set-up as an instance of our generic, tactic-based translator for specifications to code.
Thomas Meyer, Burkhart Wolff
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Authors Thomas Meyer, Burkhart Wolff
Comments (0)