F*
F*（读作“F star”）是一个由微软研究院和INRIA主导开发的、基于ML的依赖类型函数式程序语言，主要用于程序的形式化验证。
 | |
| 编程范型 | 多范式：函数式、指令式、面向对象、元编程、并发编程 |
|---|---|
| 设计者 | 微软研究院、INRIA |
| 当前版本 |
|
| 型态系统 | 静态类型、强类型、类型推断 |
| 操作系统 | Linux, macOS, Windows |
| 许可证 | Apache许可证 |
| 文件扩展名 | .fst |
| 网站 | https://fstar-lang.org/ |
| 启发语言 | |
| F#、OCaml、Standard ML、Coq、Lean、Dafny | |
F*的类型系统十分丰富，支持依赖类型、单子化效用（monadic effects）和细化类型（refinement types）。这使其能够准确地用于表述程序的形式化规范，包括功能正确性和安全性。 F*的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。
使用F*书写的程序可被编译到OCaml、F#或C加以执行。早期版本的F*亦支持编译到JavaScript。
F*语言本身使用F*和F#实现，并可从OCaml或F#引导。它的源码使用Apache协议授权，目前托管在GitHub上[2]。
引用
编辑- ^ Release 0.9.6.0. 2018年5月17日 [2022年10月4日].
- ^ FStarLang/FStar. GitHub. [2020-01-11]. （原始内容存档于2020-07-10）.
来源
编辑- Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil. Dijkstra Monads for Free. 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2017 [2021-08-29]. （原始内容存档于2022-03-02）.
- Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago. Dependent Types and Multi-Monadic Effects in F*. 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2016 [2021-08-29]. （原始内容存档于2022-04-30）.
外部链接
编辑