Paper Info
Title
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 (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.
Year
DOI
Venue
2010
10.1007/978-3-642-12251-4_9
FLOPS
Keywords
Field
DocType
dictionary translation,type class,intermediate language,mini-haskell program,higher-order logic,equational logic,data refinement concept,code generation facility,possible target,functional programming language,higher order,code generation,higher order logic
Programming language,Functional programming,Computer science,Correctness,Algorithm,Code generation,Theoretical computer science,Intermediate language,Equational logic,Type constructor,Semantics
Conference
Volume
ISSN
ISBN
6009
0302-9743
3-642-12250-7
Citations 
PageRank 
References 
54
2.00
14
Authors
2
Name
Order
Citations
PageRank
Florian Haftmann124713.39
Tobias Nipkow23056232.28