欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜：Formal mathematics/Isabelle/ML, Formal verification/Coq/Agda, C++/Erlang/Lisp
F*
来自开放百科 - 灰狐
（版本间的差异）
小 (→项目) |
小 (→文档) |
||
| （未显示1个用户的7个中间版本） | |||
| 第6行： | 第6行： | ||
==简介== | ==简介== | ||
| + | [[文件:FStarLang-logo.png|right|FStarLang]] | ||
| + | |||
F*: A Proof-oriented Programming Language, Apache License 2.0. | F*: A Proof-oriented Programming Language, Apache License 2.0. | ||
| 第11行： | 第13行： | ||
F* 的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。 | F* 的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。 | ||
| + | |||
| + | F* 是用 F* 写的，用 OCaml 引导的。一些核心文件（parser、lexer）也是直接用 [[OCaml]] 编写的。 | ||
| + | |||
| + | F* 最初是在 [[F Sharp|F#]] 中实现的。现在，F* 可以提取 F* 程序到 [[OCaml]]，F* 就被自举引导到 [[OCaml]] 中。 | ||
==功能== | ==功能== | ||
| + | *[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/tutorial/ F* tutorial] | ||
| + | *[https://www.fstar-lang.org/gs2021/gs2021.html Proof-oriented Programming in F*] | ||
==项目== | ==项目== | ||
| + | *[https://github.com/FStarLang/FStar F* @ GitHub] | ||
*[https://github.com/project-everest/hacl-star HACL*] a formally verified cryptographic library（形式化验证密码学库）written in F* | *[https://github.com/project-everest/hacl-star HACL*] a formally verified cryptographic library（形式化验证密码学库）written 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] | ||
| + | |||
| + | ==书籍== | ||
==图集== | ==图集== | ||
<gallery> | <gallery> | ||
image:FStar-Architecture.png|F*架构 | image:FStar-Architecture.png|F*架构 | ||
| + | image:FStar-for-Billions-User.png|F*服务亿万用户 | ||
</gallery> | </gallery> | ||
==链接== | ==链接== | ||
*[https://fstar-lang.org/ F*] | *[https://fstar-lang.org/ F*] | ||
| − | |||
[[category:programming language]] | [[category:programming language]] | ||
[[category:proof assistant]] | [[category:proof assistant]] | ||
| + | [[category:formal]] | ||
[[category:ML]] | [[category:ML]] | ||
[[category:F Sharp]] | [[category:F Sharp]] | ||
[[category:OCaml]] | [[category:OCaml]] | ||
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*服务亿万用户
[编辑] 链接
分享您的观点
