F * (язык программирования)

F*

Парадигма	Мультипарадигма : функциональная, императивная
Разработано	Microsoft Research и Inria
Стабильный выпуск	репозиторий
Дисциплина ввода	Зависимый, предполагаемый, статический, сильный
OS	Linux, macOS, Windows
Лицензия	Лицензия Apache 2.0
Веб-сайт	www.fstar-lang.org
Под влиянием
Coq, Дафни, F#, Lean, OCaml, Standard ML

F*(произносится F star) - это f функциональный язык программирования, вдохновленный ML и предназначенный для проверки программ. Его система типов включает зависимые типы, монадические эффекты и типы уточнения. Это позволяет выражать точные спецификации программ, включая функциональную корректность и свойства безопасности. Средство проверки типов F * стремится доказать, что программы соответствуют их спецификациям, используя комбинацию SMT-решения и ручных проверок. Программы, написанные на F *, могут быть переведены на OCaml, F# и C для выполнения. Предыдущие версии F * также могут быть переведены на JavaScript.

Последняя версия F * полностью написана в общем подмножестве F * и F #, а также в OCaml. и F #. Это открытый исходный код (под лицензией Apache License 2.0 ) и находится в стадии активной разработки на GitHub.

Источники

• Ahman, Danel; Хришку, Кэтэлин; Майярд, Кенджи; Мартинес, Гвидо; Плоткин, Гордон; Проценко, Джонатан; Растоги, Асим; Свами, Нихил (2017). "Монады Дейкстры бесплатно". 44-й симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования.
• Свами, Нихил; Хришку, Кэтэлин; Келлер, Шанталь; Растоги, Асим; Делинья-Лаво, Антуан; Форест, Саймон; Бхаргаван, Картикеян; Фурне, Седрик; Страб, Пьер-Ив; Кольвейс, Маркульф; Зинзиндохуэ, Жан-Карим; Занелла-Бегелин, Сантьяго (2016). «Зависимые типы и многомонадические эффекты в F *». 43-й симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования.

• Домашняя страница F *
• Исходный код F * на GitHub
• Учебник F *