| F* | |
|---|---|
| Clasa de limba |
multi- paradigma : funcțională , orientată pe obiecte , generalizată , programare imperativă |
| Autor | Microsoft Research și INRIA [1] |
| Dezvoltator | Microsoft Research [2] și INRIA |
| Eliberare | |
| Tip sistem | strict, static, cu inferență de tip , cu tipuri dependente |
| A fost influențat | Coq , Dafny , F# , Lean , OCaml , Standard ML |
| Licență | Licență software Apache |
| Site-ul web | fstar-lang.org |
| OS | Software multiplatform ( Linux , macOS , Windows ) |
F * (pronunțat ca F star) este un limbaj de programare funcțional bazat pe ML și axat pe verificarea formală a programelor dezvoltate pe acesta.
Sistemul său de tipuri include tipuri dependente , efecte monadice și tipuri de rafinament Aceste mijloace expresive sunt suficiente pentru a oferi specificații precise pentru programe, inclusiv descrieri ale corectitudinii funcționale și proprietăților de securitate. Mecanismul de verificare a tipului din F* vă permite să dovediți că programele sunt conforme cu specificațiile lor. Acest lucru se realizează folosind o combinație de soluție SMT și dovezi manuale . Programele scrise în F* pot fi traduse în OCaml , F# și C pentru compilare și execuție ulterioară. Versiunile anterioare de F* puteau fi traduse și în JavaScript .
Cea mai recentă versiune de F* este scrisă în întregime într-un subset comun de F* și F# și poate fi rulată folosind fie OCaml, fie F#. Codul sursă al limbii este deschis sub licența Apache 2.0 și este dezvoltat activ pe GitHub [4] .
| Microsoft Research (MSR) | |||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Principalele proiecte |
| ||||||||||||||
| Laboratoarele MSR |
| ||||||||||||||
| Categorie | |||||||||||||||
| Software gratuit și open source Microsoft | |||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| informatii generale |
| ||||||||||||
| software _ |
| ||||||||||||
| Licențe | |||||||||||||
| subiecte asemănătoare |
| ||||||||||||
| Categorie | |||||||||||||