F*
F*（讀作「F star」）是一個由微軟研究院和INRIA主導開發的、基於ML的依賴類型函數式程序語言，主要用於程序的形式化驗證。
 | |
| 編程範型 | 多範式：函數式、指令式、面向對象、元編程、並發編程 |
|---|---|
| 設計者 | 微軟研究院、INRIA |
| 當前版本 |
|
| 型態系統 | 靜態類型、強類型、類型推斷 |
| 操作系統 | Linux, macOS, Windows |
| 許可證 | Apache許可證 |
| 文件擴展名 | .fst |
| 網站 | https://fstar-lang.org/ |
| 啟發語言 | |
| F#、OCaml、Standard ML、Coq、Lean、Dafny | |
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）.
外部連結