欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/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*
[编辑] 文档
[编辑] 书籍
[编辑] 图集
[编辑] 链接
分享您的观点