Isabelle

来自开放百科 - 灰狐
（版本间的差异）
跳转到： 导航, 搜索
小
小 (→‎课程)
 
（未显示1个用户的34个中间版本）
第5行： 第5行：
  
 
==简介==
 
==简介==
 +
Lawrence C. Paulson, “Isabelle: The Next 700 Theorem Provers”
 +
 
Isabelle 是一个基于高阶逻辑（higher-order logic, HOL）的通用交互式定理证明器。它是一个 LCF（Logic for Computable Functions）风格的证明辅助工具，使用 Standard [[ML]] 语言实现，采用 BSD 许可证。它拥有一个极小化的逻辑核心；这意味着使用它的证明和形式化验证具有较强的的可信度。
 
Isabelle 是一个基于高阶逻辑（higher-order logic, HOL）的通用交互式定理证明器。它是一个 LCF（Logic for Computable Functions）风格的证明辅助工具，使用 Standard [[ML]] 语言实现，采用 BSD 许可证。它拥有一个极小化的逻辑核心；这意味着使用它的证明和形式化验证具有较强的的可信度。
  
第10行： 第12行：
  
 
Isabelle IDE 基于 [[jEdit]] 构建。
 
Isabelle IDE 基于 [[jEdit]] 构建。
 +
 +
[[Open Provable Foundation]]
  
 
==功能==
 
==功能==
 +
HOL = Functional Programming + Logic.
 +
*[https://docs.huihoo.com/proof/isabelle/isabelle2021-1/docs/implementation.pdf The Isabelle/Isar Implementation]
 +
*[https://isabelle.in.tum.de/coursematerial/PSV2009-1/session78/document.pdf Isar — A language for structured proofs]
  
 
==指南==
 
==指南==
 +
*[https://docs.huihoo.com/proof/isabelle/isabelle2021-1/docs/isar-ref.pdf The Isabelle/Isar Reference Manual]
  
 
==项目==
 
==项目==
 
[[文件:isabelle-afp.png|right|Archive of Formal Proofs]]
 
[[文件:isabelle-afp.png|right|Archive of Formal Proofs]]
 +
[[文件:Isabelle-LLVM.png|right|Isabelle-LLVM]]
 +
*[https://github.com/seL4/isabelle Isabelle @ GitHub]
 
*[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 定理形式化工作的维护通过形式化证明存档（Archive of Formal Proofs）进行，[https://www.isa-afp.org/statistics.html 截至 2022 年它已包含逾 650 个条目，约330万行证明]
+
Isabelle 定理验证维护通过形式化证明存档（Archive of Formal Proofs）方式进行着（形式证明档案是一个证明库、例子和更多科学发展的集合，在定理检验器Isabelle中机械地检查。它是以科学杂志的方式组织，提交的资料都需经过评审）[https://www.isa-afp.org/statistics.html 截至 2022.10.14 它已包含 685个条目]
 +
*[https://www21.in.tum.de/research.html Chair for Logic and Verification]
 +
*[https://github.com/lammich/isabelle_llvm Isabelle-LLVM]
 +
*[[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 团队开发了史上首个功能正确性得以形式化验证的通用操作系统内核：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。
−
*2009年，澳大利亚 NICTA 的 L4 团队开发了史上首个功能正确性得以形式化验证的通用操作系统内核：seL4 微内核。其证明使用 Isabelle/HOL 构建，包含了 200000 行证明脚本，用以验证 7500 行 C 代码。该形式化验证涵盖了代码、设计与实现，其主定理指出：该内核的 C 代码正确地实现了其形式化设计规范。
+
−
*程序语言 Lightweight Java 类型安全的形式化证明使用了 Isabelle。
+
  
 
==图集==
 
==图集==
 
<gallery>
 
<gallery>
 +
image:HOL-family-tree.png|HOL家族
 +
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实现
 +
image:isabelle-code-generator-architecture.png|代码生成器架构
 +
image:SMT-LIB-logics.png|SMT-LIB logics
 
</gallery>
 
</gallery>
  
 
==链接==
 
==链接==
 
*[https://isabelle.in.tum.de/ isabelle官网]
 
*[https://isabelle.in.tum.de/ isabelle官网]
 +
*[https://trustworthy.systems/research/formal-methods/ Trustworthy Systems Formal methods]
  
 +
[[category:formal]]
 
[[category:proof assistant]]
 
[[category:proof assistant]]
 
[[category:ML]]
 
[[category:ML]]
 
[[category:Huihoo Foundation]]
 
[[category:Huihoo Foundation]]

2022年10月14日 (五) 06:10的最后版本

Wikipedia-35x35.png 您可以在Wikipedia上了解到此条目的英文信息 Isabelle Thanks, Wikipedia.

isabelle

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 构建。

Open Provable Foundation

[编辑] 功能

HOL = Functional Programming + Logic.

[编辑] 指南

[编辑] 项目

Archive of Formal Proofs
Isabelle-LLVM

Isabelle 定理验证维护通过形式化证明存档（Archive of Formal Proofs）方式进行着（形式证明档案是一个证明库、例子和更多科学发展的集合，在定理检验器Isabelle中机械地检查。它是以科学杂志的方式组织，提交的资料都需经过评审）截至 2022.10.14 它已包含 685个条目

[编辑] 文档

[编辑] 图书

[编辑] 课程

[编辑] 案例

  • 2009年，澳大利亚 NICTA 的 L4 团队开发了史上首个功能正确性得以形式化验证的通用操作系统内核：seL4 微内核 The L4.verified Proofs 其证明使用 Isabelle/HOL 构建，包含了 200000 行证明脚本，用以验证 7500 行 C 代码。该形式化验证涵盖了代码、设计与实现，其主定理指出：该内核的 C 代码正确地实现了其形式化设计规范The seL4 Haskell Model Haskell
  • 程序语言 Lightweight Java 类型安全的形式化证明使用了 Isabelle。

[编辑] 图集

  • HOL家族

  • 系统架构

  • isabelle

  • 运行在Windows

  • isabelle插件

  • isabelle实现

  • 代码生成器架构

  • SMT-LIB logics

[编辑] 链接

来自“http://wiki.huihoo.com/wiki/?title=Isabelle&oldid=166106”
分享您的观点
个人工具
名字空间

变换
操作
导航
工具箱