Code Generation via Higher-Order Rewrite Systems

Florian Haftmann Tobias Nipkow

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 and the intermediate language, both are given a semantics in terms of higher-order rewrite systems. In a second step, type classes are removed from 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.



author={Florian Haftmann and Tobias Nipkow},
title={Code Generation via Higher-Order Rewrite Systems},
booktitle={Functional and Logic Programming (FLOPS 2010)},
editor={M. Blume and N. Kobayashi and G. Vidal},