A Compiled Implementation of Normalization by Evaluation

Klaus Aehlig Florian Haftmann Tobias Nipkow

We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open lambda-terms w.r.t. 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.



author={Klaus Aehlig and Florian Haftmann and Tobias Nipkow},
title={A Compiled Implementation of Normalization by Evaluation},
journal={Journal of Functional Programming},
Isabelle theories in the Archive of Formal Proofs

This is an extended version of this conference paper.