@inproceedings{6c8fbde64a964d4d98cb620850168a26,
title = "A compiled implementation of normalization by evaluation",
abstract = "We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normalization of open λ-terms w.r.t. β-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",
year = "2008",
doi = "10.1007/978-3-540-71067-7_8",
language = "English",
isbn = "3540710655",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "39--54",
booktitle = "Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings",
note = "21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008 ; Conference date: 18-08-2008 Through 21-08-2008",
}