Sciweavers

Share
TPHOL
2008
IEEE

A Compiled Implementation of Normalization by Evaluation

8 years 9 months ago
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.
Klaus Aehlig, Florian Haftmann, Tobias Nipkow
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Klaus Aehlig, Florian Haftmann, Tobias Nipkow
Comments (0)
books