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.

• Type: Conference
• Year: 2004
• Where: TYPES
• Authors: Thomas Meyer, Burkhart Wolff
• Keywords: Corresponding Operational Semantics, Formal Methods, Optimized Compilation, Particular Instance, TYPES 2004