F* (プログラミング言語)

F* (F スター) はプログラム検証を目的とした、MLに影響を受けた関数型プログラミング言語である。型システムには依存型、モナディックエフェクトの要素が組み込まれており、それによりプログラムの詳細な仕様を型で表現することができる。F*の型検査機はプログラムが仕様を満たすことをSMT solvingと手動証明を組み合わせて証明する。F*のプログラムはOCaml、F#、C言語に変換され実行される。

F*

F*のロゴ
パラダイム	マルチパラダイム: 関数型言語, 命令型言語, 形式検証
最新リリース	repository
型付け	static, strong, inferred, dependent types, formal verification
影響を受けた言語	F#, OCaml, Standard ML, Fine, F7, F5, FX, HTT, Trellys, Zombie, Dafny
プラットフォーム	クロスプラットフォーム (Windows、macOS, Linux)
ライセンス	Apache 2.0 License
ウェブサイト	www.fstar-lang.org
拡張子	.fst