A compiled implementation of normalization by evaluation
- Klaus Aehlig
- Florian Haftmann
- Tobias Nipkow
Publication date
January 2008
DOI Publisher
Springer-Verlag ISSN
0302-9743 Citation count (estimate)
13Abstract
Abstract. We present a novel compiled approach to Normalization by Evaluation (NBE) for ML-like languages. It supports efficient normal-ization of open λ-terms w.r.t. β-reduction and rewrite rules. We have implemented NBE and show both a detailed formal model of our imple-mentation and its verification in Isabelle. Finally we discuss how NBE is turned into a proof rule in Isabelle.
Add to ORKG