BibTeX:
@inproceedings{AehligHN-TPHOLs08, author={Klaus Aehlig and Florian Haftmann and Tobias Nipkow}, title={A Compiled Implementation of Normalization by Evaluation}, booktitle={Theorem Proving in Higher Order Logics (TPHOLs 2008)}, editor={Ait Mohamed and Munoz and Tahar}, publisher={Springer},series={LNCS},volume={5170},pages={39-54},year=2008}Isabelle theories in the Archive of Formal Proofs
This paper has been superseded by an extended journal version.