F * (pronunciado F estrella ) es un lenguaje de programación funcional inspirado en ML y destinado a la verificación de programas . Su sistema de tipos incluye tipos dependientes , efectos monádicos y tipos de refinamiento . Esto permite expresar especificaciones precisas para los programas, incluida la corrección funcional y las propiedades de seguridad. El verificador de tipo F * tiene como objetivo demostrar que los programas cumplen con sus especificaciones utilizando una combinación de resolución SMT y pruebas manuales . Los programas escritos en F * se pueden traducir a OCaml , F # y Cpara su ejecución. Las versiones anteriores de F * también se pueden traducir a JavaScript .
Paradigma | Multi-paradigma : funcional , imperativo |
---|---|
Diseñada por | Microsoft Research e Inria [1] |
Lanzamiento estable | |
Disciplina de mecanografía | Dependiente , inferido , estático , fuerte |
SO | Linux , macOS , Windows |
Licencia | Licencia Apache 2.0 |
Sitio web | www |
Influenciado por | |
Coq , Dafny , F # , Lean , OCaml , ML estándar |
La última versión de F * está escrita completamente en un subconjunto común de F * y F # , y arranca tanto en OCaml como en F # . Es de código abierto (bajo la licencia Apache 2.0 ) y está en desarrollo activo en GitHub . [2]
Referencias
- ^ "Centro conjunto de Microsoft Research Inria" . MSR-INRIA .
- ^ "FStarLang / FStar" . GitHub .
Fuentes
- Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Dijkstra Monads gratis" . 44º Simposio ACM SIGPLAN-SIGACT sobre Principios de Lenguajes de Programación .
- Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Bosque, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago (2016). "Tipos dependientes y efectos multimónádicos en F *" . 43º Simposio ACM SIGPLAN-SIGACT sobre Principios de Lenguajes de Programación .
enlaces externos
- F * Página de inicio
- Código fuente F * en GitHub
- F * tutorial