Florian Haftmann (itestra GmbH), Tobias Nipkow
Code Generation via Higher-Order Rewrite Systems
Functional and Logic Programming, 10th International Symposium, FLOPS 2010, Sendai, Japan, April 19 - 21, 2010.
Abstract
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 (HRSs). 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 re nement concept.
