Tactic-based optimized compilation of functional programs

Within a framework of correct code-generation from HOL-specifications, 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.