Code Generation via Higher-Order Rewrite Systems

We present the meta-theory behind the code generation facilities of Isabelle/HOL. To bridge the gap between the source (higher-order logic with type classes) and the many possible targets (functional programming languages), we introduce an intermediate language, Mini-Haskell. To relate the source mid the intermediate language, both are given a semantics in terms of higher-order rewrite systems (HRSs). In a second step, type classes are removed hoot Mini-Haskell programs by means of a dictionary translation; we prove the correctness of this step. Building on equational logic also directly supports a simple but powerful algorithm and data refinement concept.