https://wiki.taigi.ima.org.tw/w/index.php?action=history&feed=atom&title=F%2A 2026-04-08T01:58:35Z 本 wiki 上此頁面的修訂紀錄 MediaWiki 1.43.1 https://wiki.taigi.ima.org.tw/w/index.php?title=F*&diff=420004&oldid=prev 2025-08-22T13:28:31Z

<p>從 JSON 檔案批量匯入</p> <p><b>新頁面</b></p><div>&#039;&#039;&#039;F \&#039;&#039;&#039;*（讀作「F star」）是一个小可仔軟軟研究院佮 INRIA 主導開發的、是因為 ML 的依賴類型函數式程序語言，主要是用佇程序的形式化驗證。<br /> <br /> F \ * 的類型系統十分豐富，支持依賴類型、單仔化效用（monadic effects）佮細化類型（refinement types）。 這其實會當準確地用佇表述程序的形式化規範，包括功能正確性佮安全性。<br /> F \ * 的類型檢查器通過檢查手寫的證明佮 SMT 自動求解來確保程序符合規範。<br /> <br /> 使用 F \ * 書寫的程序會當予人編譯到 OCaml、F # 抑是 C 加以執行。早期版本的 F \ * 支持編譯到 JavaScript。<br /> <br /> F \ * 語言本身使用 F \ * 和 F # 實現，並會使對 OCaml 抑是 F # 引導。伊的源碼用 Apache 協議授權，目前託管佇 GitHub 上。<br /> <br /> ==引用==<br /> <br /> ===來源===<br /> <br /> * 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 . 二千空一十七 [二千空二十一孵八堵二十九] .（原始內容存檔佇兩千空二十二抹三鋪二）.<br /> * 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 . 二千空一十六 [二千空二十一孵八堵二十九] .（原始內容存檔佇兩千空二十二抹四四配三十）.<br /> <br /> ==外部連結==<br /> <br /> * F \ * 官方主頁<br /> * F \ * 源碼<br /> * F \ * 教程<br /> <br /> [[分類: 待校正]]</div>

TaiwanTonguesApiRobot