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.

• Type: Conference
• Year: 2010
• Where: FLOPS
• Authors: Florian Haftmann, Tobias Nipkow
• Keywords: Code Generation Facilities, FLOPS 2010, Hardware, Intermediate Language, Type Classes