Isabelle/HOL实际应用示例
An example of pratical application of Isabelle/HOL
我查看了 Isabelle 教程，其中提供了一个使用它来验证安全协议的示例。但是，这有点超出我的理解，因为我只知道基础知识。我正在寻找一些示例，这些示例不仅是简单的定理，而且是使用 Isabelle/HOL 的实际应用。
例如证明一些算法或可能是验证属性系统或一些非平凡的数学定理。这样的例子在任何地方都可用吗？
我查看了 isabelle 官方页面中提供的所有应用程序列表，但大多数都是定理证明。
我也在查看使用 Alloy 进行文件系统验证的示例。它提供了可以验证 file/directories 的属性的证明。我正在寻找类似的东西。
我现在能想到的几个非常重要的例子是：
seL4，一个完整的操作系统内核，用 C 编写，并经过 Isabelle 验证。
据我所知，AFP 条目 Jinja_Threads 包含一个完全形式化的字节码编译器，用于具有数组和线程的 Java 类语言。
Jeremy Avigad 对 Prime Number Theorem.
的证明
Kepler's conjecture的证明。其中一部分是在伊莎贝尔完成的；然而，其中大部分是在更“基本”的定理证明器 HOL Light 中完成的，其逻辑类似于 Isabelle。
正如 Joachim 提到的，我相信您可以在 AFP
中找到更多有趣的应用程序
我查看了 Isabelle 教程，其中提供了一个使用它来验证安全协议的示例。但是，这有点超出我的理解，因为我只知道基础知识。我正在寻找一些示例，这些示例不仅是简单的定理，而且是使用 Isabelle/HOL 的实际应用。 例如证明一些算法或可能是验证属性系统或一些非平凡的数学定理。这样的例子在任何地方都可用吗？
我查看了 isabelle 官方页面中提供的所有应用程序列表，但大多数都是定理证明。
我也在查看使用 Alloy 进行文件系统验证的示例。它提供了可以验证 file/directories 的属性的证明。我正在寻找类似的东西。
我现在能想到的几个非常重要的例子是：
seL4，一个完整的操作系统内核，用 C 编写，并经过 Isabelle 验证。
据我所知，AFP 条目 Jinja_Threads 包含一个完全形式化的字节码编译器，用于具有数组和线程的 Java 类语言。
Jeremy Avigad 对 Prime Number Theorem.
的证明Kepler's conjecture的证明。其中一部分是在伊莎贝尔完成的；然而，其中大部分是在更“基本”的定理证明器 HOL Light 中完成的，其逻辑类似于 Isabelle。
正如 Joachim 提到的，我相信您可以在 AFP
中找到更多有趣的应用程序