跳至內容

F*

維基百科,自由的百科全書
F*
編程範型多範式函數式指令式面向對象元編程並發編程
設計者微軟研究院INRIA
當前版本
  • 0.9.6.0(2018年5月17日)[1]
編輯維基數據鏈接
型態系統靜態類型強類型類型推斷
作業系統Linux, macOS, Windows
許可證Apache許可證
文件擴展名.fst
網站https://fstar-lang.org/
啟發語言
F#OCamlStandard MLCoqLean英語Lean (proof assistant)Dafny英語Dafny

F*(讀作「F star」)是一個由微軟研究院INRIA主導開發的、基於ML依賴類型函數式程序語言,主要用於程序的形式化驗證。

F*的類型系統十分豐富,支持依賴類型、單子化效用(monadic effects)和細化類型(refinement types)。這使其能夠準確地用於表述程序的形式化規範,包括功能正確性和安全性。 F*的類型檢查器通過檢查手寫的證明和SMT自動求解來確保程序符合規範。

使用F*書寫的程序可被編譯到OCamlF#C加以執行。早期版本的F*亦支持編譯到JavaScript。

F*語言本身使用F*和F#實現,並可從OCamlF#引導。它的源碼使用Apache協議授權,目前託管在GitHub[2]

引用

  1. ^ Release 0.9.6.0. 2018年5月17日 [2022年10月4日]. 
  2. ^ 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). 

外部連結