Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants
Correctness of Isabelle's Cyclicity Checker: Implementability of Overloading in Proof Assistants
复制标题
Isabelle 循环检查器的正确性：证明助手中重载的可实现性
DOI：
10.1145/2676724.2693175
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Ondřej Kunčar
中科院分区：
文献类型：
--
作者：
Ondřej Kunčar
重载常量定义是证明助手 Isabelle 的一个重要功能，因为它们允许我们向用户提供类似 Haskell 的类型类。一直存在一个问题，即在什么条件下我们实际上可以保证重载是一种安全的理论扩展，即保持一致性或保守。自然条件是由重载定义生成的重写系统必须始终终止。当前系统对接受的重载定义施加限制，并通过属于 Isabelle 可信代码库一部分的算法来决定终止。因此，我们的目标是证明它的正确性。由于我们的工作，我们不仅发现了完整性缺陷，而且还发现了正确性问题——我们可以证明错误。在我们的论文中，我们提出了该算法的修改版本以及其完整性和正确性的证明。虽然我们的工作涉及 Isabelle，但我们的论文提供了更通用的结果：如何在证明助手中实际实现重载。
Overloaded constant definitions are an important feature of the proof assistant Isabelle because they allow us to provide Haskell-like type classes to our users. There has been an ongoing question as to under which conditions we can practically guarantee that overloading is a safe theory extension, i.e., preserves consistency or is conservative. The natural condition is that a rewriting system generated by overloaded definitions must always terminate. The current system imposes restrictions on accepted overloaded definitions and decides the termination by an algorithm that is part of the trusted code base of Isabelle. Therefore we aim to prove its correctness.Thanks to our work we discovered not only completeness shortcomings but also a correctness issue---we could prove False. In our paper we present a modified version of the algorithm together with a proof of completeness and correctness of it.Although our work deals with Isabelle, our paper provides a more general result: how to practically implement overloading in proof assistants.
登录
查看更多内容
DOI：
10.1007/11805618_16
发表时间：
2006
期刊：
Arch. Formal Proofs
影响因子：
--
作者：
Steven Obua
通讯作者：
Steven Obua
高阶逻辑中的类型类和重载
DOI：
10.1007/bfb0028402
发表时间：
1997
期刊：
Proceedings of the 9th Workshop on Programming Languages and Operating Systems
影响因子：
--
作者：
M. Wenzel
通讯作者：
M. Wenzel
开阳简而言之
DOI：
10.6092/issn.1972-5787/1980
发表时间：
2010
期刊：
J. Formaliz. Reason.
影响因子：
--
作者：
Adam Grabowski;Artur Korniłowicz;Adam Naumowicz
通讯作者：
Adam Naumowicz
伊莎贝尔的构造类型类
DOI：
10.1007/978-3-540-74464-1_11
发表时间：
2006
期刊：
J. Formaliz. Reason.
影响因子：
--
作者：
Florian Haftmann;M. Wenzel
通讯作者：
M. Wenzel
具有子类型的 Lambda 演算的约简和统一
DOI：
--
发表时间：
1992
期刊：
CADE
影响因子：
--
作者：
T. Nipkow;Zhenyu Qian
通讯作者：
Zhenyu Qian