<分区>
我正在为 Isabelle2013/HOL 寻找可免费获得的优质教程和文档(除了经过 Google 搜索和挖掘后显而易见的那些)。你能推荐一些吗？
标签 isabelle
<分区>
我正在为 Isabelle2013/HOL 寻找可免费获得的优质教程和文档(除了经过 Google 搜索和挖掘后显而易见的那些)。你能推荐一些吗？
最佳答案
一些可以帮助您入门的文档:
之前的实际教程是 A Proof Assistant for Higher-Order Logic由 Nipkow、Paulson 和 Wenzel 撰写。本文档介绍了 Isabelle/HOL 作为一种函数式编程语言，并提供了有关如何使用 Isabelle/HOL 中可用的大多数常见证明机制的指南。这是一个很好的起点；
较新的教程是 Programming and Proving in Isabelle/HOL尼普科夫。它涵盖了一些与以前的文档相同的 Material ，但没有那么深入，但使用了更现代的技术在 Isabelle/HOL 中进行证明。它可以作为 Isabelle/HOL 的“快速入门”。
免费书籍 Concrete Semantics Nipkow 和 Klein 着，在对编程语言执行证明的上下文中介绍了 Isabelle/HOL。如果您对 Isabelle/HOL 的兴趣在于程序验证，那么这本书将是一个好的开始。
一般来说，大多数(但不是全部)好的引用指南都链接到 Isabelle documentation page本身。但是请注意，因为其中一些文档已经很旧并且不太可能再相关了(尽管这些文档已被标记为此类)。
网络上还有大量的幻灯片和讲义，例如 UNSW或 University of Edinburgh ，但这些可能更适合用作补充，因为它们通常缺少讲座中提供的上下文和重要细节。
关于需要 Isabelle/HOL 教程/文档，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/19905683/