必要的Isabelle/HOL教程/文档

Question

我正在为Isabelle2013/HOL寻找免费的、高质量的教程和文档(除了Google-ing和挖掘一点之后明显的那些教程和文档)。你能给我推荐一些吗？

Answer 1

一些可能帮助您入门的文档：

• 上一篇事实上的教程是由尼普考、保尔森和温泽尔编写的高阶逻辑的证明助手。本文件介绍了Isabelle/HOL作为一种函数式编程语言，以及关于如何使用Isabelle/HOL中提供的大多数常见证明机制的指南。这是一个很好的起点；
• 一个较新的教程是Nipkow的在Isabelle/HOL中的编程和证明。它涵盖了一些与前一份文件相同的材料，不太深入，但使用了更现代的技术来执行伊莎贝尔/霍尔的证明。对伊莎贝尔/霍尔来说，这可能是一个“快速启动”。
• 由Nipkow和Klein免费提供的书具体语义提供了伊莎贝尔/霍尔在对编程语言进行证明的背景下的介绍。如果您对Isabelle/HOL的兴趣与程序验证有关，这本书将是一个很好的开始。

一般情况下，大多数(但不是所有)好的参考指南都是从伊莎贝尔文件页本身链接到的。不过，请注意，因为其中一些文件相当古老，不太可能再有关联(尽管这类文件已被标记为如此)。

网站上也有大量的幻灯片和讲稿，如新南威尔士或爱丁堡大学，但它们可能更好地作为一种补充，因为它们通常缺乏上下文和在讲座中提供的重要细节。