A Consistent Foundation for Isabelle/HOL
A Consistent Foundation for Isabelle/HOL
复制标题
Isabelle/HOL 的一致基础
DOI：
10.1007/s10817-018-9454-8
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
A. Popescu
中科院分区：
文献类型：
--
作者：
Ondrej Kuncar;A. Popescu
交互定理证明者Isabelle/HOL基于被广泛理解的高阶逻辑（HOL），它被广泛认为是一致的（并且通过标准语义论证在集合论中可证明一致）。然而，Isabelle/HOL为HOL带来了自己的个人风格：重载常量定义，用于为用户提供类似haskell的类型类。这些特性对用户来说是一种乐趣，但不幸的是，作为hol的扩展，它们不容易正确使用——它们有不一致的行为历史。在何种标准下，重载常量定义和类型定义可以组合在一起，同时仍然保证一致性，这一直是一个悬而未决的问题。本文提出了解决这一问题的方法：定义不重叠和定义依赖关系的终止（不仅通过常量跟踪，而且通过类型跟踪）确保了Isabelle/HOL的相对一致性。
The interactive theorem prover Isabelle/HOL is based on the well understood higher-order logic (HOL), which is widely believed to be consistent (and provably consistent in set theory by a standard semantic argument). However, Isabelle/HOL brings its own personal touch to HOL: overloaded constant definitions, used to provide the users with Haskell-like type classes. These features are a delight for the users, but unfortunately are not easy to get right as an extension of HOL—they have a history of inconsistent behavior. It has been an open question under which criteria overloaded constant definitions and type definitions can be combined together while still guaranteeing consistency. This paper presents a solution to this problem: non-overlapping definitions and termination of the definition-dependency relation (tracked not only through constants but also through types) ensures relative consistency of Isabelle/HOL.
登录
查看更多内容
Isabelle 循环检查器的正确性：证明助手中重载的可实现性
DOI：
10.1145/2676724.2693175
发表时间：
2015
期刊：
Proceedings of the 2015 Conference on Certified Programs and Proofs
影响因子：
--
作者：
Ondřej Kunčar
通讯作者：
Ondřej Kunčar
理解 Isabelle/HOL 的一致性
DOI：
10.1007/978-3-662-54434-1_27
发表时间：
2017
期刊：
影响因子：
--
作者：
Ondřej Kunčar;Andrei Popescu
通讯作者：
Andrei Popescu
HOL 和 Isabelle/HOL 中定义的安全性和保守性
影响因子：
--
作者：
Ondřej Kunčar;Andrei Popescu
通讯作者：
Andrei Popescu
基础可扩展核心递归：证明助理的观点
DOI：
10.1145/2784731.2784732
发表时间：
2015
期刊：
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Jasmin Christian Blanchette;Andrei Popescu;Dmitriy Traytel
通讯作者：
Dmitriy Traytel