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 |
---|
テンプレートを表示 |
F* (F スター) はプログラム検証を目的とした、MLに影響を受けた関数型プログラミング言語である。型システムには依存型、モナディックエフェクトの要素が組み込まれており、それによりプログラムの詳細な仕様を型で表現することができる。F*の型検査機はプログラムが仕様を満たすことをSMT solvingと手動証明を組み合わせて証明する。F*のプログラムはOCaml、F#、C言語に変換され実行される。
- Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Dijkstra Monads for Free". 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
- Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves (2016). "Dependent Types and Multi-Monadic Effects in F*". 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.