欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/Agda, C++/Erlang/Lisp
F*
来自开放百科 - 灰狐
（版本间的差异）
小 (→指南) |
小 (→文档) |
||
| （未显示1个用户的4个中间版本） | |||
| 第19行： | 第19行： | ||
==功能== | ==功能== | ||
| + | *[https://www.fstar-lang.org/gs2021/gs2021.html#/sec-types-are-specifications-total-functions-are-proofs-recursion-is-induction Types are specifications; Total functions are proofs; Recursion is induction（递归是归纳法）] | ||
==指南== | ==指南== | ||
| − | [https://www.fstar-lang.org/gs2021/gs2021.html Proof-oriented Programming in F*] | + | *[https://www.fstar-lang.org/tutorial/ F* tutorial] |
| + | *[https://www.fstar-lang.org/gs2021/gs2021.html Proof-oriented Programming in F*] | ||
==项目== | ==项目== | ||
| 第29行： | 第31行： | ||
==文档== | ==文档== | ||
*[https://www.fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf Proof-Oriented Programming in F*] | *[https://www.fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf Proof-Oriented Programming in F*] | ||
| − | + | *[https://fstar-lang.org/papers/metafstar/metafstar-slides-esop2019.pdf Meta-F* Proof Automation with SMT, Tactics, and Metaprograms] | |
==书籍== | ==书籍== | ||
| 第36行： | 第38行： | ||
<gallery> | <gallery> | ||
image:FStar-Architecture.png|F*架构 | image:FStar-Architecture.png|F*架构 | ||
| + | image:FStar-for-Billions-User.png|F*服务亿万用户 | ||
</gallery> | </gallery> | ||
2023年8月1日 (二) 02:37的最后版本
|
您可以在Wikipedia上了解到此条目的英文信息 F* Thanks, Wikipedia. |
F*
目录 |
[编辑] 简介
F*: A Proof-oriented Programming Language, Apache License 2.0.
F*（F star）是一个由微软研究院和 INRIA 主导开发的、基于ML的依赖类型函数式程序语言，主要用于程序的形式化验证。
F* 的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。
F* 是用 F* 写的，用 OCaml 引导的。一些核心文件（parser、lexer）也是直接用 OCaml 编写的。
F* 最初是在 F# 中实现的。现在，F* 可以提取 F* 程序到 OCaml，F* 就被自举引导到 OCaml 中。
[编辑] 功能
[编辑] 指南
[编辑] 项目
- F* @ GitHub
- HACL* a formally verified cryptographic library（形式化验证密码学库）written in F*
[编辑] 文档
[编辑] 书籍
[编辑] 图集
F*架构
F*服务亿万用户
[编辑] 链接
分享您的观点
