F*（プログラミング言語）

F* ( Fスターと発音) は、ML、Caml、OCaml 言語に触発された、高水準のマルチパラダイム関数型オブジェクト指向プログラミング言語で、プログラム検証を目的としています。これは、 Microsoft Researchとフランス国立情報学研究所(Inria)の共同プロジェクトです。 ^[¹^]その型システムには、依存型、モナド効果、およびリファインメント型が含まれています。これにより、機能的正しさやセキュリティ特性を含む、プログラムの正確な仕様を表現できます。F* 型チェッカーは、充足可能性モジュロ理論(SMT) の解決と手動証明の組み合わせを使用して、プログラムが仕様を満たしていることを証明することを目指しています。実行のために、F* で書かれたプログラムは、OCaml、F#、C、WebAssembly (KaRaMeL ツール経由)、またはアセンブリ言語(Vale ツールチェーン経由) に変換できます。以前の F* バージョンはJavaScriptに変換することもできました。

これは2011年に導入され^{[ 3 ]}^{[ 4 ]} 、 GitHubで活発に開発されている^[²^]。

歴史

バージョン 2022.03.24 までは、F* は F* とF#の共通サブセットで完全に記述されており、 OCamlと F#の両方でブートストラップをサポートしていました。これはバージョン 2022.04.02 から廃止されました。^{[ 5 ]}^{[ 6 ]}

F* は、、、、などの一般的な算術演算子をサポートしています。また、F *は、、、、、、などの関係演算子もサポートしています。^[⁷^]+-*/<<===!=>>=

F* の一般的な基本データ型boolは、、、、、およびです。^[⁷^]intfloatcharunit

1 2 「マイクロソフトリサーチインリアジョイントセンター」MSR-INRIA。
1 2 "FStarLang/FStar" . GitHub . 2026年4月26日のオリジナルからアーカイブ済み. 2026年4月26日取得.
↑ Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean (2011年9月).値依存型による安全な分散プログラミング. ICFP '11: 第16回ACM SIGPLAN国際関数型プログラミング会議議事録. Vol. 46. 東京、日本: Association for Computing Machinery. pp. 266–278 . doi : 10.1145 /2034574.2034811 . 2023年4月17日取得.
↑ 「F*プロジェクト」。マイクロソフト。 2023年4月20日取得。
↑ "fstar.exe は F# で .NET 実行ファイルとしてビルドできなくなりました #2512" . Github . 2023 年4 月 17 日取得.
↑ 「F* コードが有効な F# でなければならないという要件を削除することを検討する #1737」。Github。2023年4月17 日取得。
1 2 Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024年1月14日). F* における証明指向プログラミング(PDF)。

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 .
スワミー、ニキル。フリシュク、カタリン;ケラー、シャンタル。ラストギ、アシーム。デリニャ・ラヴォー、アントワーヌ。フォレスト、サイモン。バーガヴァン、カーティケヤン。フルネ、セドリック。ストルブ、ピエール＝イヴ。コールワイス、マルクルフ。ジンジンドゥエ、ジャン＝カリム。ザネラ・ベグリン、サンティアゴ（2016）。「F* における依存型とマルチモナディック効果」。プログラミング言語の原則に関する第 43 回 ACM SIGPLAN-SIGACT シンポジウム。
Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024). F* における証明指向プログラミング。