| F* | |
|---|---|
 | |
| Класс языка |
мультипарадигменный: функциональное, объектно-ориентированное, обобщённое, императивное программирование |
| Автор | Microsoft Research и INRIA[1] |
| Разработчик | Microsoft Research[2] и INRIA |
| Выпуск | |
| Система типов | строгая, статическая, с выводом типов, с зависимыми типами |
| Испытал влияние | Coq, Dafny, F#, Lean, OCaml, Standard ML |
| Лицензия | Apache Software License |
| Сайт | fstar-lang.org |
| ОС | Кроссплатформенное программное обеспечение (Linux, macOS, Windows) |
F * (произносится как F star) — функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ.
Его система типов включает в себя зависимые типы, монадические эффекты и типы-уточнения. Этих выразительных средств достаточно, чтобы задавать точные спецификации для программ, включая описания функциональной корректности и свойств безопасности. Механизм проверки типов в F* позволяет доказывать, что программы соответствуют их спецификациям. Это делается с использованием комбинации SMT-решателя и ручных доказательств. Программы, написанные на F*, могут быть странслированы в OCaml, F# и C для дальнейшей компиляции и выполнения. Предыдущие версии F* также можно было транслировать в JavaScript.
Последняя версия F* написана полностью на общем подмножестве F* и F# и может быть запущена как с использованием OCaml, так и с использованием F#. Исходный код языка открыт под лицензией Apache 2.0 и активно разрабатывается на GitHub[4].
Энциклопедичный YouTube
-
1/5Просмотров:2 73923 903164 66680749 250
-
F.LUX - ЛУЧШАЯ ПРОГРАММА ДЛЯ СОХРАНЕНИЯ ГЛАЗ!ОБЗОР ПРОГРАММ!
-
Будилов С. А. "Активация природных программ"
-
Программы выбираются, а стирка не начинается
-
Аксиоматический метод верификации программ А. Хоара
-
А.Т.Фоменко в программе "Предметный разговор"
Субтитры
Литература
- Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Dijkstra Monads for Free". 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
- 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 (2016). "Dependent Types and Multi-Monadic Effects in F*". 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
Ссылки
| Основные проекты |
| ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| MSR Labs |
| ||||||||||||||
| Общая информация |
| ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Программное обеспечение |
| ||||||||||||
| Лицензии | |||||||||||||
| Связанные темы |
| ||||||||||||
Примечания
- ↑ Microsoft Research Inria Joint Centre. MSR-INRIA. Дата обращения: 28 мая 2020. Архивировано 21 мая 2020 года.
- ↑ 1 2 https://www.fstar-lang.org/#people
- ↑ Release 0.9.6.0 — 2018.
- ↑ FStarLang/FStar. GitHub. Дата обращения: 28 мая 2020. Архивировано 10 июля 2020 года.
Эта страница в последний раз была отредактирована 19 декабря 2023 в 13:12.
Обычно почти сразу, изредка в течении часа.