A compiled implementation of normalisation by evaluation

Klaus Aehlig; Florian Haftmann; Tobias Nipkow

doi:10.1017/S0956796812000019

A compiled implementation of normalisation by evaluation

Klaus Aehlig, Florian Haftmann, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Research output: Contribution to journal › Article › peer-review

8 Scopus citations

Abstract

We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open λ-terms with respect to β-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
Pages (from-to)	9-30
Number of pages	22
Journal	Journal of Functional Programming
Volume	22
Issue number	1
DOIs	https://doi.org/10.1017/S0956796812000019
State	Published - Jan 2012

Access to Document

10.1017/S0956796812000019

Cite this

@article{27e1576c709c4d889401e78f328e2778,

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

abstract = "We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open λ-terms with respect to β-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",

note = "Funding Information: This is a revised and extended version of (Aehlig et al., 2008). † Supported by DFG Grant Ni 491/10 1 Available online at afp.sf.net",

year = "2012",

month = jan,

doi = "10.1017/S0956796812000019",

language = "English",

volume = "22",

pages = "9--30",

journal = "Journal of Functional Programming",

issn = "0956-7968",

publisher = "Cambridge University Press",

number = "1",

}

TY - JOUR

T1 - A compiled implementation of normalisation by evaluation

AU - Aehlig, Klaus

AU - Haftmann, Florian

AU - Nipkow, Tobias

N1 - Funding Information: This is a revised and extended version of (Aehlig et al., 2008). † Supported by DFG Grant Ni 491/10 1 Available online at afp.sf.net

PY - 2012/1

Y1 - 2012/1

N2 - We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open λ-terms with respect to β-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 Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open λ-terms with respect to β-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=84858817506&partnerID=8YFLogxK

U2 - 10.1017/S0956796812000019

DO - 10.1017/S0956796812000019

M3 - Article

AN - SCOPUS:84858817506

SN - 0956-7968

VL - 22

SP - 9

EP - 30

JO - Journal of Functional Programming

JF - Journal of Functional Programming

IS - 1

ER -

A compiled implementation of normalisation by evaluation

Abstract

Access to Document

Other files and links

Fingerprint

Cite this