F*

F \*（讀作「F star」）是一个小可仔軟軟研究院佮 INRIA 主導開發的、是因為 ML 的依賴類型函數式程序語言，主要是用佇程序的形式化驗證。

F \ * 的類型系統十分豐富，支持依賴類型、單仔化效用（monadic effects）佮細化類型（refinement types）。 這其實會當準確地用佇表述程序的形式化規範，包括功能正確性佮安全性。 F \ * 的類型檢查器通過檢查手寫的證明佮 SMT 自動求解來確保程序符合規範。

使用 F \ * 書寫的程序會當予人編譯到 OCaml、F # 抑是 C 加以執行。早期版本的 F \ * 支持編譯到 JavaScript。

F \ * 語言本身使用 F \ * 和 F # 實現，並會使對 OCaml 抑是 F # 引導。伊的源碼用 Apache 協議授權，目前託管佇 GitHub 上。

引用

來源

• Ahman , Danel ; Hriţcu , Cătălin ; Maillard , Kenji ; Martínez , Guido ; Plotkin , Gordon ; Protzenko , Jonathan ; Rastogi , Aseem ; Swamy , Nikhil . Dijkstra Monads for Free . 四十四 nd 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 ; Kohlweiss , Markulf ; Zinzindohoue , Jean-Karim ; Zanella-Béguelin , Santiago . Dependent Types and Multi-Monadic Effects in F \ * . 四十三 nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . 二千空一十六 [二千空二十一孵八堵二十九] .（原始內容存檔佇兩千空二十二抹四四配三十）.

外部連結

• F \ * 官方主頁
• F \ * 源碼
• F \ * 教程