A Compiled Implementation of Normalization by Evaluation

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.

• Type: Conference
• Year: 2008
• Where: TPHOL
• Authors: Klaus Aehlig, Florian Haftmann, Tobias Nipkow
• Keywords: Artificial Intelligence, Efficient Normalization, ML-like Languages, Rewrite Rules, TPHOL 2008