Open Provable Foundation

2022年6月8日 (三) 09:31的版本

Open Provable Foundation（开放可证明基础）

Provably Awesome
ML 语言家族适用于形式语言、计算机辅助定理证明、证明助理、逻辑语言、一阶逻辑、论证软件、代码验证等形式化领域。
Haskell, Agda, Idris, Liquid Haskell 具有“证明即程序、命题为类型”的特征。
F*
ACL2
proof assistant
Coq
Isabelle
HOL = functional programming + logic HOL Interactive Theorem Prover 文档 HOL Theory Hierarchy (Theory Graph)
seL4 The world's most highly assured OS kernel, specification and proofs with isabelle. The seL4 Haskell Model Haskell
Hardware description language for Formal verification

@@ 第23行： / 第23行： @@
 *[[Coq]]
 *[[Isabelle]]
-*[https://hol-theorem-prover.org/ HOL Interactive Theorem Prover] [https://docs.huihoo.com/proof/hol-interactive-theorem-prover/ 文档] [https://docs.huihoo.com/proof/hol-interactive-theorem-prover/kananaskis-14-helpdocs/help/theorygraph/theories.html HOL Theory Hierarchy (Theory Graph)]
+*HOL = functional programming + logic [https://hol-theorem-prover.org/ HOL Interactive Theorem Prover] [https://docs.huihoo.com/proof/hol-interactive-theorem-prover/ 文档] [https://docs.huihoo.com/proof/hol-interactive-theorem-prover/kananaskis-14-helpdocs/help/theorygraph/theories.html HOL Theory Hierarchy (Theory Graph)]
 *[https://github.com/seL4/l4v seL4] The world's most highly assured OS kernel, specification and proofs with isabelle. [https://github.com/seL4/l4v/tree/master/spec/haskell The seL4 Haskell Model] [[Haskell]]
 *[[Hardware description language]] for [[Formal verification]]