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 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.
pdf
BibTeX:
@inproceedings{HaftmannN-FLOPS2010,
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},
publisher=Springer,series=LNCS,volume={6009},pages={103-117},year=2010}