Article contents
A compiled implementation of normalisation by evaluation*
Published online by Cambridge University Press: 29 February 2012
Abstract
We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open λ-terms with respect to β-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
- Articles
- Information
- Copyright
- Copyright © Cambridge University Press 2012
References
- 4
- Cited by
Discussions
No Discussions have been published for this article.