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

редактировать
F*
Fstar-official-logo-2015.png
Парадигма Мультипарадигма : функциональная, императивная
Разработано 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 по принципам языков программирования.

Внешние ссылки

Последняя правка сделана 2021-05-20 06:10:43
Содержание доступно по лицензии CC BY-SA 3.0 (если не указано иное).
Обратная связь: support@alphapedia.ru
Соглашение
О проекте