Code generation via higher-order rewrite systems. (English) Zbl 1284.68131

Haftmann, Florian; Nipkow, Tobias

Blume, Matthias (ed.) et al., Functional and logic programming. 10th international symposium, FLOPS 2010, Sendai, Japan, April 19–21, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-12250-7/pbk). Lecture Notes in Computer Science 6009, 103-117 (2010).

Summary: 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 refinement concept.
For the entire collection see [Zbl 1186.68003].

MSC:

68N18	Functional programming and lambda calculus
68Q42	Grammars and rewriting systems
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

CeTA; Isabelle/HOL; Haskell