A compiled implementation of normalization by evaluation

Klaus Aehlig; Florian Haftmann; Tobias Nipkow

doi:10.1007/978-3-540-71067-7_8

A compiled implementation of normalization by evaluation

Klaus Aehlig, Florian Haftmann, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

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

9 Scopus citations

Abstract

We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normalization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.

Original language	English
Title of host publication	Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings
Publisher	Springer Verlag
Pages	39-54
Number of pages	16
ISBN (Print)	3540710655, 9783540710653
DOIs	https://doi.org/10.1007/978-3-540-71067-7_8
State	Published - 2008
Event	21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008 - Montreal, QC, Canada Duration: 18 Aug 2008 → 21 Aug 2008

Publication series

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

Conference

Conference	21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008
Country/Territory	Canada
City	Montreal, QC
Period	18/08/08 → 21/08/08

Access to Document

10.1007/978-3-540-71067-7_8

Cite this

Aehlig, K., Haftmann, F., & Nipkow, T. (2008). A compiled implementation of normalization by evaluation. In Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings (pp. 39-54). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5170 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_8

Aehlig, Klaus ; Haftmann, Florian ; Nipkow, Tobias. / A compiled implementation of normalization by evaluation. Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, 2008. pp. 39-54 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6c8fbde64a964d4d98cb620850168a26,

title = "A compiled implementation of normalization by evaluation",

abstract = "We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normalization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.",

author = "Klaus Aehlig and Florian Haftmann and Tobias Nipkow",

year = "2008",

doi = "10.1007/978-3-540-71067-7_8",

language = "English",

isbn = "3540710655",

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

publisher = "Springer Verlag",

pages = "39--54",

booktitle = "Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings",

note = "21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008 ; Conference date: 18-08-2008 Through 21-08-2008",

}

Aehlig, K, Haftmann, F & Nipkow, T 2008, A compiled implementation of normalization by evaluation. in Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5170 LNCS, Springer Verlag, pp. 39-54, 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008, Montreal, QC, Canada, 18/08/08. https://doi.org/10.1007/978-3-540-71067-7_8

A compiled implementation of normalization by evaluation. / Aehlig, Klaus; Haftmann, Florian; Nipkow, Tobias.
Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, 2008. p. 39-54 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5170 LNCS).

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

TY - GEN

T1 - A compiled implementation of normalization by evaluation

AU - Aehlig, Klaus

AU - Haftmann, Florian

AU - Nipkow, Tobias

PY - 2008

Y1 - 2008

N2 - We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normalization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.

AB - We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normalization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our implementation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.

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

U2 - 10.1007/978-3-540-71067-7_8

DO - 10.1007/978-3-540-71067-7_8

M3 - Conference contribution

AN - SCOPUS:57049166562

SN - 3540710655

SN - 9783540710653

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

SP - 39

EP - 54

BT - Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings

PB - Springer Verlag

T2 - 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008

Y2 - 18 August 2008 through 21 August 2008

ER -

Aehlig K, Haftmann F, Nipkow T. A compiled implementation of normalization by evaluation. In Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag. 2008. p. 39-54. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-71067-7_8

A compiled implementation of normalization by evaluation

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this