https://arolstar52-zhtest.hf.space/index.php?action=history&feed=atom&title=F%2A F* - 版本历史 2026-07-18T02:10:39Z 在这个wiki上该页的修订历史 MediaWiki 1.43.9 https://arolstar52-zhtest.hf.space/index.php?title=F*&diff=2281131&oldid=prev imported>ExultantEditor 来自 2025年12月26日 (五) 16:55 2025-12-26T16:55:42Z <p></p> <p><b>新页面</b></p><div>{{Infobox programming language<br /> | name = F*<br /> | logo = Fstar-official-logo-2015.png<br /> | logo_size = 160px<br /> | caption = <br /> | file_ext = &lt;code&gt;.fst&lt;/code&gt;<br /> | paradigm = [[多范式]]：[[函数式编程|函数式]]、[[指令式编程|指令式]]、[[面向对象的程序设计|面向对象]]、[[元编程]]、[[并发计算|并发编程]]<br /> | designer = [[微软研究院]]、[[法国国家信息与自动化研究所|INRIA]]<br /> | developer = <br /> | latest_release_version = v2021.07.31<br /> | latest_release_date = {{start date|2021|07|31}}<br /> | latest_preview_version = <br /> | latest_preview_date = <br /> | typing = [[静态类型]]、[[强类型]]、[[类型推断]]<br /> | implementations = <br /> | dialects = <br /> | influenced_by = [[F♯|F#]]、[[OCaml]]、[[Standard ML]]、[[Coq]]、{{le|Lean (证明辅助)|Lean (proof assistant)|Lean}}、{{le|Dafny}}<br /> | influenced = <br /> | operating_system = [[Linux]], [[macOS]], [[Windows]]<br /> | license = [[Apache许可证]]<br /> | website = https://fstar-lang.org/<br /> }}<br /> <br /> &#039;&#039;&#039;F*&#039;&#039;&#039;（读作“F star”）是一个由[[微软研究院]]和[[法国国家信息与自动化研究所|INRIA]]主导开发的、基于[[ML语言|ML]]的[[依赖类型]][[函数式编程|函数式]][[程序语言]]，主要用于程序的形式化验证。<br /> <br /> F*的类型系统十分丰富，支持[[依赖类型]]、单子化效用（monadic effects）和细化类型（refinement types）。这使其能够准确地用于表述程序的形式化规范，包括功能正确性和安全性。<br /> F*的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。<br /> <br /> 使用F*书写的程序可被编译到[[OCaml]]、[[F♯|F#]]或[[C语言|C]]加以执行。早期版本的F*亦支持编译到JavaScript。<br /> <br /> F*语言本身使用F*和[[F♯|F#]]实现，并可从[[OCaml]]或[[F♯|F#]]引导。它的源码使用[[Apache协议]]授权，目前托管在[[GitHub]]上&lt;ref&gt;{{cite web|url=https://github.com/FStarLang/FStar|title=FStarLang/FStar|website=GitHub|access-date=2020-01-11|archive-date=2020-07-10|archive-url=https://web.archive.org/web/20200710025302/https://github.com/FStarLang/FStar}}&lt;/ref&gt;。<br /> <br /> ==引用==<br /> {{reflist}}<br /> ===来源===<br /> * {{cite conference<br /> | first1 = Danel<br /> | last1 = Ahman<br /> | first2 = Cătălin<br /> | last2 = Hriţcu<br /> | first3 = Kenji<br /> | last3 = Maillard<br /> | first4 = Guido<br /> | last4 = Martínez<br /> | first5 = Gordon<br /> | last5 = Plotkin<br /> | first6 = Jonathan<br /> | last6 = Protzenko<br /> | first7 = Aseem<br /> | last7 = Rastogi<br /> | first8 = Nikhil<br /> | last8 = Swamy<br /> | title = Dijkstra Monads for Free<br /> | url = https://www.fstar-lang.org/papers/dm4free/<br /> | book-title = 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages<br /> | year = 2017<br /> | access-date = 2021-08-29<br /> | archive-date = 2022-03-02<br /> | archive-url = https://web.archive.org/web/20220302183006/https://www.fstar-lang.org/papers/dm4free/<br /> }}<br /> * {{cite conference<br /> | first1 = Nikhil<br /> | last1 = Swamy<br /> | first2 = Cătălin<br /> | last2 = Hriţcu<br /> | first3 = Chantal<br /> | last3 = Keller<br /> | first4 = Aseem<br /> | last4 = Rastogi<br /> | first5 = Antoine<br /> | last5 = Delignat-Lavaud<br /> | first6 = Simon<br /> | last6 = Forest<br /> | first7 = Karthikeyan<br /> | last7 = Bhargavan<br /> | first8 = Cédric<br /> | last8 = Fournet<br /> | first9 = Pierre-Yves<br /> | last9 = Strub<br /> | first10 = Markulf<br /> | last10 = Kohlweiss<br /> | first11 = Jean-Karim<br /> | last11 = Zinzindohoue<br /> | first12 = Santiago<br /> | last12 = Zanella-Béguelin<br /> | title = Dependent Types and Multi-Monadic Effects in F*<br /> | url = https://www.fstar-lang.org/papers/mumon/<br /> | book-title = 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages<br /> | year = 2016<br /> | access-date = 2021-08-29<br /> | archive-date = 2022-04-30<br /> | archive-url = https://web.archive.org/web/20220430082919/https://www.fstar-lang.org/papers/mumon/<br /> }}<br /> <br /> == 外部链接 ==<br /> *[https://www.fstar-lang.org/ F* 官方主页]{{Wayback|url=https://www.fstar-lang.org/ |date=20200331073002 }}<br /> * [https://github.com/FStarLang/FStar F* 源码]{{Wayback|url=https://github.com/FStarLang/FStar |date=20200710025302 }}<br /> * [https://www.fstar-lang.org/tutorial/ F* 教程]{{Wayback|url=https://www.fstar-lang.org/tutorial/ |date=20200512022900 }}<br /> <br /> <br /> {{程序设计语言|Logo}}<br /> [[Category:微软研究院]]<br /> [[Category:程序设计语言]]<br /> [[Category:ML語言家族]]<br /> [[Category:.NET编程语言]]</div> imported>ExultantEditor