欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
Isabelle
来自开放百科 - 灰狐
(版本间的差异)
小 (→项目) |
小 (→图书) |
||
(未显示1个用户的14个中间版本) | |||
第29行: | 第29行: | ||
*[https://isabelle-dev.sketis.net/source/isabelle/ Isabelle @ Phabricator] | *[https://isabelle-dev.sketis.net/source/isabelle/ Isabelle @ Phabricator] | ||
*[https://www.isa-afp.org/ Isabelle 形式化证明存档(Archive of Formal Proofs)] | *[https://www.isa-afp.org/ Isabelle 形式化证明存档(Archive of Formal Proofs)] | ||
− | Isabelle | + | Isabelle 定理验证维护通过形式化证明存档(Archive of Formal Proofs)方式进行着(形式证明档案是一个证明库、例子和更多科学发展的集合,在定理检验器Isabelle中机械地检查。它是以科学杂志的方式组织,提交的资料都需经过评审)[https://www.isa-afp.org/statistics.html 截至 2024.08.12 它已包含 838个条目] |
+ | *[https://www21.in.tum.de/research.html Chair for Logic and Verification] | ||
*[https://github.com/lammich/isabelle_llvm Isabelle-LLVM] | *[https://github.com/lammich/isabelle_llvm Isabelle-LLVM] | ||
*[[Cardano]] [https://github.com/input-output-hk/fm-ledger-formalization Ledger formalization] | *[[Cardano]] [https://github.com/input-output-hk/fm-ledger-formalization Ledger formalization] | ||
+ | *[https://github.com/au-ts/cogent Cogent] Code and Proof Co-Generation | ||
+ | *[https://www.polyml.org/ Poly/ML] 是 Standard [[ML]] 的开源高效实现,支持 Isabelle 和 [https://hol-theorem-prover.org/ HOL4] | ||
+ | *[https://isarmathlib.org/ IsarMathLib] Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant | ||
+ | |||
+ | ==文档== | ||
+ | |||
+ | ==图书== | ||
+ | *[http://concrete-semantics.org/concrete-semantics.pdf 《Concrete Semantics with Isabelle/HOL》] [http://concrete-semantics.org/index.html Concrete Semantics] | ||
+ | |||
+ | ==课程== | ||
+ | *[http://cs4161.web.cse.unsw.edu.au/ Advanced Topics in Software Verification] | ||
+ | *[https://www21.in.tum.de/teaching.html Teaching - Chair for Logic and Verification] | ||
+ | *[https://www21.in.tum.de/teaching/logic/SS22/index.html Propositional logic and First-order logic] | ||
==案例== | ==案例== | ||
− | *2009年,澳大利亚 NICTA 的 L4 | + | *2009年,澳大利亚 NICTA 的 L4 团队开发了史上首个功能正确性得以形式化验证的通用操作系统内核:seL4 微内核 [https://github.com/seL4/l4v The L4.verified Proofs] 其证明使用 Isabelle/HOL 构建,包含了 200000 行证明脚本,用以验证 7500 行 C 代码。该形式化验证涵盖了代码、设计与实现,其主定理指出:该内核的 C 代码正确地实现了其[https://github.com/seL4/l4v/tree/master/spec 形式化设计规范][https://github.com/seL4/l4v/tree/master/spec/haskell The seL4 Haskell Model] [[Haskell]] |
*程序语言 Lightweight [[Java]] 类型安全的形式化证明使用了 Isabelle。 | *程序语言 Lightweight [[Java]] 类型安全的形式化证明使用了 Isabelle。 | ||
第43行: | 第57行: | ||
image:isabelle-system-architecture.png|系统架构 | image:isabelle-system-architecture.png|系统架构 | ||
image:isabelle.png|isabelle | image:isabelle.png|isabelle | ||
+ | image:isabelle-on-windows.png|运行在Windows | ||
image:isabelle-plugin-manager.png|isabelle插件 | image:isabelle-plugin-manager.png|isabelle插件 | ||
image:isabelle-implementation.png|isabelle实现 | image:isabelle-implementation.png|isabelle实现 |
2024年8月12日 (一) 00:17的最后版本
您可以在Wikipedia上了解到此条目的英文信息 Isabelle Thanks, Wikipedia. |
isabelle
目录 |
[编辑] 简介
Lawrence C. Paulson, “Isabelle: The Next 700 Theorem Provers”
Isabelle 是一个基于高阶逻辑(higher-order logic, HOL)的通用交互式定理证明器。它是一个 LCF(Logic for Computable Functions)风格的证明辅助工具,使用 Standard ML 语言实现,采用 BSD 许可证。它拥有一个极小化的逻辑核心;这意味着使用它的证明和形式化验证具有较强的的可信度。
Isabelle 被用于形式化数学和计算机科学中的许多定理,诸如哥德尔完备性定理、哥德尔关于选择公理一致性的证明、素数定理、各种安全协议的正确性、程序语言语义的特性。
Isabelle IDE 基于 jEdit 构建。
[编辑] 功能
HOL = Functional Programming + Logic.
[编辑] 指南
[编辑] 项目
Isabelle 定理验证维护通过形式化证明存档(Archive of Formal Proofs)方式进行着(形式证明档案是一个证明库、例子和更多科学发展的集合,在定理检验器Isabelle中机械地检查。它是以科学杂志的方式组织,提交的资料都需经过评审)截至 2024.08.12 它已包含 838个条目
- Chair for Logic and Verification
- Isabelle-LLVM
- Cardano Ledger formalization
- Cogent Code and Proof Co-Generation
- Poly/ML 是 Standard ML 的开源高效实现,支持 Isabelle 和 HOL4
- IsarMathLib Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant
[编辑] 文档
[编辑] 图书
[编辑] 课程
- Advanced Topics in Software Verification
- Teaching - Chair for Logic and Verification
- Propositional logic and First-order logic
[编辑] 案例
- 2009年,澳大利亚 NICTA 的 L4 团队开发了史上首个功能正确性得以形式化验证的通用操作系统内核:seL4 微内核 The L4.verified Proofs 其证明使用 Isabelle/HOL 构建,包含了 200000 行证明脚本,用以验证 7500 行 C 代码。该形式化验证涵盖了代码、设计与实现,其主定理指出:该内核的 C 代码正确地实现了其形式化设计规范The seL4 Haskell Model Haskell
- 程序语言 Lightweight Java 类型安全的形式化证明使用了 Isabelle。
[编辑] 图集
[编辑] 链接
分享您的观点