问Isabelle/HOL中的验证器核心

EN

伊莎贝尔是"LCF系列“证明检查器的一员，这意味着你有一个特殊的模块--推理内核--所有的推理都通过它来产生抽象数据类型thm的值。这有点像操作系统内核处理系统调用。相对于内核实现的正确性，您可以以这种方式生成的一切都是“构造正确的”。由于验证器的编程语言环境(Standard )具有很强的静态类型正确性特性，推理内核的构造正确性将传递给其他的验证辅助实现，这可能是相当大的。

因此，原则上，您有一个相对较小的“可信内核”部分和一个非常大的“应用程序用户空间”。特别是，大多数Isabelle/HOL实际上是一个大量的图书馆理论和附加工具(主要是在SML中)在伊莎贝尔的用户土地。

在Isabelle中，内核基础结构非常复杂，但与系统的其他部分相比仍然非常小。内核实际上是分层为“微内核”(模块)和“纳米内核”(模块)。Thm生成米尔纳的LCF-方法意义上的thm值，Context为您生成的任何结果处理theory证书，以及本地推理的证明上下文(特别是在Isar证明语言中)。

如果你想了解更多关于LCF风格的证明，我建议你也看看荷-光，它可能是LCF家族中最小的现实系统，在某种意义上是现实的，因为人们已经用它做了大量的应用。HOL-Light有一个很大的优势，它的实现可以很容易理解，但这种极简主义也有一些轻蔑的优点:它不能完全保护用户在它的ML环境(即OCaml而不是SML )中做无意义的事情。由于各种技术原因，OCaml在默认情况下并不像标准ML那样“安全”。

如果你解开伊莎贝尔的消息来源，比如。

linux.tar.gz

您将在

src/Pure/thm.ML

而且，有这样一个项目，你已经想要解决：

http://www.proof-technologies.com/holzero/

稍后添加:另一个更严重的项目是

https://team.inria.fr/parsifal/proofcert/