Theorem Proving in Higher Order Logics
Theorem Proving in Higher Order Logics
复制标题
高阶逻辑中的定理证明
DOI：
10.1007/978-3-540-71067-7_8
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Aehlig K
中科院分区：
文献类型：
--
作者：
Aehlig K
我们提出了一种新的编译方法，用于类ml语言的归一化评估（NBE）。它支持开放λ项w.r.t.b β-约简和重写规则的有效规范化。我们已经实现了NBE，并在Isabelle中展示了我们的实现及其验证的详细正式模型。最后讨论了《伊莎贝尔》中NBE如何转化为证明规则。
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.