Sciweavers

TYPES
2004
Springer

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
Where TYPES
Authors Thomas Meyer, Burkhart Wolff
Comments (0)