科研之友
微信
新浪微博
Facebook
分享链接
摘要
We present a novel compiled approach to Normalisation by Evaluation (NBE) for ML-like languages. It supports efficient normalisation of open lambda-terms with respect to beta-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.
- 出版日期2012-1
