Code Generation via Higher-Order Rewrite Systems

14 years 1 months ago
Code Generation via Higher-Order Rewrite Systems
Abstract. We present the meta-theory behind the code generation facilities of Isabelle/HOL. To bridge the gap between the source (higherorder logic with type classes) and the many possible targets (functional programming languages), we introduce an intermediate language, MiniHaskell. 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.
Florian Haftmann, Tobias Nipkow
Added 18 May 2010
Updated 18 May 2010
Type Conference
Year 2010
Authors Florian Haftmann, Tobias Nipkow
Comments (0)