F*

维基百科,自由的百科全书
跳到导航 跳到搜索
F*
Fstar-official-logo-2015.png
编程范型多范式函数式指令式面向对象元编程并发编程
設計者微软研究院INRIA
穩定版本
v2021.07.31
( 2021年7月31日 (2021-07-31)
型態系統静态类型强类型类型推断
作業系統Linux, macOS, Windows
許可證Apache许可证
文件扩展名.fst
網站https://fstar-lang.org/
啟發語言
F#OCamlStandard MLCoqLean英语Lean (proof assistant)Dafny英语Dafny

F*(读作“F star”)是一个由微软研究院INRIA主导开发的、基于ML依赖类型函数式程序语言,主要用于程序的形式化验证。

F*的类型系统十分丰富,支持依赖类型、单子化效用(monadic effects)和细化类型(refinement types)。这使其能够准确地用于表述程序的形式化规范,包括功能正确性和安全性。 F*的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。

使用F*书写的程序可被编译到OCamlF#C加以执行。早期版本的F*亦支持编译到JavaScript。

F*语言本身使用F*和F#实现,并可从OCamlF#引导。它的源码使用Apache协议授权,目前托管在GitHub[1]

引用[编辑]

  1. ^ 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). 

外部链接[编辑]