http://wikihandbk.com/ruwiki/index.php?action=history&feed=atom&title=%D0%90%D0%BD%D0%B3%D0%BB%D0%B8%D0%B9%D1%81%D0%BA%D0%B0%D1%8F_%D0%92%D0%B8%D0%BA%D0%B8%D0%BF%D0%B5%D0%B4%D0%B8%D1%8F%3AF%2A_%28programming_language%29 2026-10-02T00:06:06Z История изменений этой страницы в вики MediaWiki 1.40.0 http://wikihandbk.com/ruwiki/index.php?title=%D0%90%D0%BD%D0%B3%D0%BB%D0%B8%D0%B9%D1%81%D0%BA%D0%B0%D1%8F_%D0%92%D0%B8%D0%BA%D0%B8%D0%BF%D0%B5%D0%B4%D0%B8%D1%8F:F*_(programming_language)&diff=14635347&oldid=prev 2024-03-05T17:23:52Z

<p>Новая страница: «{{Английская Википедия/Панель перехода}} {{Short description|Functional programming language inspired by ML and aimed at program verification}} {{distinguish|F (programming language)}} {{Infobox programming language | name = F* | logo = Fstar-official-logo-2015.png | logo_size = 128px | caption = | paradigm = multi-paradigm programming language|M...»</p> <p><b>Новая страница</b></p><div>{{Английская Википедия/Панель перехода}}<br /> {{Short description|Functional programming language inspired by ML and aimed at program verification}}<br /> {{distinguish|F (programming language)}}<br /> {{Infobox programming language<br /> | name = F*<br /> | logo = Fstar-official-logo-2015.png<br /> | logo_size = 128px<br /> | caption = <br /> | paradigm = [[multi-paradigm programming language|Multi-paradigm]]: [[functional programming|functional]], [[imperative programming|imperative]]<br /> | latest release version = [https://github.com/FStarLang/FStar repository]<br /> | latest release date = <br /> | typing = [[Dependent types|Dependent]], [[type inference|inferred]], [[static typing|static]], [[strong typing|strong]]<br /> | implementations = <br /> | dialects = <br /> | influenced by = [[Coq (software)|Coq]], [[Dafny (programming language)|Dafny]], [[F Sharp (programming language)|F#]], [[Lean (proof assistant)|Lean]], [[OCaml]], [[Standard ML]]<br /> | influenced =<br /> | programming language = <br /> | operating system = [[Linux]], [[macOS]], [[Windows]]<br /> | license = [[Apache License 2.0]]<br /> | website = {{url|https://www.fstar-lang.org/}}<br /> | file ext = <br /> | designers = [[Microsoft Research]] and [[Inria]]&lt;ref&gt;{{cite web|url=https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/|title=Microsoft Research Inria Joint Centre|website=MSR-INRIA}}&lt;/ref&gt;<br /> | file_ext = .fst<br /> }}<br /> <br /> '''F*''' (pronounced ''F star'') is a [[functional programming language]] inspired by [[ML (programming language)|ML]] and aimed at [[program verification]]. Its [[type system]] includes [[dependent types]], [[Monad (functional programming)|monadic]] [[side effect (computer science)|effects]], and [[refinement type]]s. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of [[satisfiability modulo theories|SMT solving]] and [[proof assistant|manual proofs]].<br /> Programs written in F* can be translated to [[OCaml]], [[F Sharp (programming language)|F#]], and [[C (programming language)|C]] for execution. Previous versions of F* could also be translated to [[JavaScript]].<br /> <br /> It was introduced in 2011&lt;ref name=&quot;origin-paper&quot;&gt;<br /> {{cite conference <br /> |last1=Swamy <br /> |first1=Nikhil <br /> |last2=Chen <br /> |first2=Juan <br /> |last3=Fournet <br /> |first3=Cédric <br /> |last4=Strub <br /> |first4=Pierre-Yves <br /> |last5=Bhargavan <br /> |first5=Karthikeyan <br /> |last6=Yang <br /> |first6=Jean <br /> |title=Secure distributed programming with value-dependent types <br /> |conference=ICFP '11: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming <br /> |date=September 2011 <br /> |volume=46 <br /> |issue=9 <br /> |pages=266–278 <br /> |location = Tokyo, Japan<br /> |doi=10.1145/2034574.2034811 <br /> |publisher=Association for Computing Machinery<br /> |url=https://dl.acm.org/doi/10.1145/2034773.2034811<br /> |access-date=17 April 2023}}&lt;/ref&gt;&lt;ref&gt;{{cite web|url= https://www.microsoft.com/en-us/research/project/the-f-project/|title= The F* Project|website=Microsoft | access-date= 20 April 2023}}&lt;/ref&gt; and is under active development on [[GitHub]].&lt;ref&gt;{{cite web|url=https://github.com/FStarLang/FStar|title=FStarLang/FStar|website=GitHub|access-date=17 April 2023 }}&lt;/ref&gt;<br /> <br /> ==History==<br /> ===Versions===<br /> Up until version 2022.03.24 F* was written entirely in a common subset of F* and [[F Sharp (programming language)|F#]] and supported bootstrapping in both [[OCaml]] and [[F Sharp (programming language)|F#]]. This was dropped beginning in version 2022.04.02.&lt;ref&gt;{{cite web |title=fstar.exe is no longer buildable in F# as a .NET executable #2512 |url=https://github.com/FStarLang/FStar/pull/2512 |website=Github |access-date=17 April 2023}}&lt;/ref&gt;&lt;ref&gt;{{cite web |title=Consider dropping requirement that F* code has to be valid F# #1737 |url=https://github.com/FStarLang/FStar/issues/1737 |website=Github |access-date=17 April 2023}}&lt;/ref&gt;<br /> <br /> ==References==<br /> {{Reflist}}<br /> <br /> ===Sources===<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 /> }}<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 /> }}<br /> <br /> ==External links==<br /> *{{Official website|www.fstar-lang.org}}<br /> *{{GitHub|FStarLang}}<br /> *[https://www.fstar-lang.org/tutorial/ F* tutorial]<br /> <br /> {{ML programming}}<br /> {{Microsoft FOSS}}<br /> {{Microsoft development tools}}<br /> {{Microsoft Research}}<br /> <br /> {{DEFAULTSORT:F star (programming language)}}<br /> [[Category:Functional languages]]<br /> [[Category:ML programming language family]]<br /> [[Category:.NET programming languages]]<br /> [[Category:Microsoft programming languages]]<br /> [[Category:Microsoft Research]]<br /> [[Category:Dependently typed languages]]<br /> [[Category:Automated theorem proving]]<br /> [[Category:Programming languages created in 2011]]<br /> [[Category:Proof assistants]]<br /> [[Category:2011 software]]<br /> <br /> {{Prog-lang-stub}}<br /> {{Навигационная таблица/Портал/Английская Википедия}}<br /> [[Категория:Английская Википедия]]<br /> [[Категория:Википедия]]<br /> [[Категория:Статья из Википедии]]<br /> [[Категория:Статья из Английской Википедии]]</div>

EducationBot