@article {IOPORT.06085234,
    author       = {Aehlig, Klaus and Haftmann, Florian and Nipkow, Tobias},
    title        = {A compiled implementation of normalisation by evaluation.},
    year         = {2012},
    journal      = {Journal of Functional Programming},
    volume       = {22},
    number       = {1},
    issn         = {0956-7968},
    pages        = {9-30},
    publisher    = {Cambridge University Press, Cambridge},
    doi          = {10.1017/S0956796812000019},
    abstract     = {Summary: We present a novel compiled approach to normalisation by evaluation (NBE) for ML-like languages. It supports efficient normalisation of open $\lambda$-terms with respect to $\beta$-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.},
    identifier   = {06085234},
}