F*

F*
编程范型	多た范式：函数かんすう式しき、指令しれい式しき、面めん向こう对象、元もと编程、并发编程
設計せっけい者しゃ	微ほろ软研究けんきゅう院いん、INRIA
当とう前ぜん版本はんぽん	0.9.6.0 (2018年ねん5月がつ17日にち);
型かた態たい系統けいとう	静せい态类型がた、强つよ类型、类型推断すいだん
操作そうさ系けい统	Linux, macOS, Windows
許可きょか證しょう	Apache许可证
文ぶん件けん扩展名めい	.fst
網あみ站	https://fstar-lang.org/
啟發けいはつ語ご言げん
	F#、OCaml、Standard ML、Coq、Lean（英えい语：Lean (proof assistant)）、Dafny（英えい语：Dafny）

F*（读作“F star”）是ぜ一いち个由微ほろ软研究けんきゅう院いん和わINRIA主しゅ导开发的、基もと于ML的てき依よ赖类型がた函数かんすう式しき程ほど序じょ语言，主要しゅよう用よう于程序じょ的てき形式けいしき化か验证。

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）.

外部がいぶ链接

[wikidata-1f7fd54c1cfbe04994ad9864d26b73fbca0cf9e9-v3-1] Release 0.9.6.0. 2018年ねん5月がつ17日にち [2022年ねん10月がつ4日にち].

[2] FStarLang/FStar. GitHub. [2020-01-11]. （原始げんし内容ないよう存そん档于2020-07-10）.

[1]

[2]