Code generation via higher-order rewrite systems

Florian Haftmann; Tobias Nipkow

doi:10.1007/978-3-642-12251-4_9

Code generation via higher-order rewrite systems

Florian Haftmann, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

137 Scopus citations

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, 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.

Original language	English
Title of host publication	Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings
Pages	103-117
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-12251-4_9
State	Published - 2010
Event	10th International Symposium on Functional and Logic Programming, FLOPS 2010 - Sendai, Japan Duration: 19 Apr 2010 → 21 Apr 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6009 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	10th International Symposium on Functional and Logic Programming, FLOPS 2010
Country/Territory	Japan
City	Sendai
Period	19/04/10 → 21/04/10

Access to Document

10.1007/978-3-642-12251-4_9

Cite this

Haftmann, F., & Nipkow, T. (2010). Code generation via higher-order rewrite systems. In Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings (pp. 103-117). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6009 LNCS). https://doi.org/10.1007/978-3-642-12251-4_9

@inproceedings{66998981728b40d3a2a86efc1fd9481e,

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 (higherorder 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.",

author = "Florian Haftmann and Tobias Nipkow",

year = "2010",

doi = "10.1007/978-3-642-12251-4_9",

language = "English",

isbn = "3642122507",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "103--117",

booktitle = "Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings",

note = "10th International Symposium on Functional and Logic Programming, FLOPS 2010 ; Conference date: 19-04-2010 Through 21-04-2010",

}

Haftmann, F & Nipkow, T 2010, Code generation via higher-order rewrite systems. in Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6009 LNCS, pp. 103-117, 10th International Symposium on Functional and Logic Programming, FLOPS 2010, Sendai, Japan, 19/04/10. https://doi.org/10.1007/978-3-642-12251-4_9

Code generation via higher-order rewrite systems. / Haftmann, Florian; Nipkow, Tobias.
Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings. 2010. p. 103-117 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6009 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Code generation via higher-order rewrite systems

AU - Haftmann, Florian

AU - Nipkow, Tobias

PY - 2010

Y1 - 2010

N2 - 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, 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.

AB - 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, 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.

UR - http://www.scopus.com/inward/record.url?scp=78651250973&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-12251-4_9

DO - 10.1007/978-3-642-12251-4_9

M3 - Conference contribution

AN - SCOPUS:78651250973

SN - 3642122507

SN - 9783642122507

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 103

EP - 117

BT - Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings

T2 - 10th International Symposium on Functional and Logic Programming, FLOPS 2010

Y2 - 19 April 2010 through 21 April 2010

ER -

Code generation via higher-order rewrite systems

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this