A Compiled Implementation of Normalization by Evaluation
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.
pdf
BibTeX:
@article{AehligHN-JFP12,
author={Klaus Aehlig and Florian Haftmann and Tobias Nipkow},
title={A Compiled Implementation of Normalization by Evaluation},
journal={Journal of Functional Programming},
volume=22,number=1,pages={9-30},year=2012}
Isabelle theories in the
Archive of Formal Proofs
This is an extended version of this conference paper.