Abstract:

Tactic-based Optimized Compilation of Functional Programs

Thomas Meyer and Burkhart Wolff


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.