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

Ф*
	Официальный логотип Fstar
Парадигма	Мультипарадигмальность : функциональная , императивная.
Семья	ML : Caml : OCaml
Разработано	Нихил Свами, Хуан Чен, Седрик Фурне, Пьер-Ив Струб, Картикеян Бхаргаван, Жан Ян
Разработчики	Исследования Майкрософт , ; Инрия
Впервые появился	2011 год ; 13 лет назад
Стабильная версия	v2023.09.03 / 3 сентября 2023 г .; 9 месяцев назад
Дисциплина набора текста	зависимый , предполагаемый , статичный , сильный
Язык реализации	Ф*
ТЫ	Кроссплатформенность : Linux , macOS , Windows.
Лицензия	Апач 2.0
Расширения имен файлов	.fst
Веб-сайт	fstar-lang .org
Под влиянием
	Coq , Dafny , F# , Lean , OCaml , Standard ML

F* (произносится как F star ) — высокоуровневый , многопарадигмальный , функциональный и объектно-ориентированный язык программирования , созданный на основе языков ML , Caml и OCaml и предназначенный для проверки программ . Это совместный проект Microsoft Research и Французского института исследований в области компьютерных наук и автоматизации (Inria). ^[1]Его система типов включает зависимые типы , монадические эффекты и уточняющие типы . Это позволяет выразить точные характеристики программ, включая функциональную корректность и свойства безопасности. Средство проверки типов F* направлено на то, чтобы доказать, что программы соответствуют их спецификациям, используя комбинацию решения по модулю выполнимости (SMT) и ручных доказательств . Для выполнения программы, написанные на F*, можно перевести на OCaml , F# , C , WebAssembly (с помощью инструмента KaRaMeL) или на язык ассемблера (с помощью цепочки инструментов Vale). Предыдущие версии F* также можно было перевести на JavaScript .

Он был представлен в 2011 году. ^[3]^[4] и находится в активной разработке на GitHub . ^[2]

История [ править ]

Версии [ править ]

До версии 2022.03.24 F* был полностью написан на общем подмножестве F* и F# и поддерживал загрузку как в OCaml , так и в F#. Начиная с версии 2022.04.02 это было исключено. ^[5]^[6]

Обзор [ править ]

Операторы [ править ]

F* поддерживает распространенные арифметические операторы , такие как +, -, *, и /. Кроме того, F* поддерживает операторы отношения, такие как <, <=, ==, !=, >, и >=. ^[7]

Типы данных [ править ]

Общие типы данных примитивов в F*: bool, int, float, char, и unit. ^[7]

Ссылки [ править ]

^ Перейти обратно: ^а ^б «Объединенный центр Microsoft Research Inria» . МСР-ИНРИА .
^ Перейти обратно: ^а ^б «ФСтарЛанг/ФСтар» . Гитхаб . Проверено 23 апреля 2024 г.
^ Свами, Нихил; Чен, Хуан; Фурне, Седрик; Струб, Пьер-Ив; Бхаргаван, Картикеян; Ян, Жан (сентябрь 2011 г.). Безопасное распределенное программирование с использованием типов, зависящих от значения . ICFP '11: Материалы 16-й Международной конференции ACM SIGPLAN по функциональному программированию. Том. 46. Токио, Япония: Ассоциация вычислительной техники. стр. 266–278. дои : 10.1145/2034574.2034811 . Проверено 17 апреля 2023 г.
^ «Проект F*» . Майкрософт . Проверено 20 апреля 2023 г.
^ «fstar.exe больше нельзя собирать на F# как исполняемый файл .NET #2512» . Гитхаб . Проверено 17 апреля 2023 г.
^ «Рассмотрите возможность исключения требования о том, что код F* должен быть действительным F# #1737» . Гитхаб . Проверено 17 апреля 2023 г.
^ Перейти обратно: ^а ^б Свами, Нихил; Мартинес, Гвидо; Растоги, Асим (14 января 2024 г.). Доказательство-ориентированное программирование на F* (PDF) .

Источники [ править ]

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

Внешние ссылки [ править ]

Эта языкам программирования, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее .

[MS-Inria-1] Перейти обратно: ^а ^б «Объединенный центр Microsoft Research Inria» . МСР-ИНРИА .

[GitHubCode-2] Перейти обратно: ^а ^б «ФСтарЛанг/ФСтар» . Гитхаб . Проверено 23 апреля 2024 г.

[origin-paper-3] Свами, Нихил; Чен, Хуан; Фурне, Седрик; Струб, Пьер-Ив; Бхаргаван, Картикеян; Ян, Жан (сентябрь 2011 г.). Безопасное распределенное программирование с использованием типов, зависящих от значения . ICFP '11: Материалы 16-й Международной конференции ACM SIGPLAN по функциональному программированию. Том. 46. Токио, Япония: Ассоциация вычислительной техники. стр. 266–278. дои : 10.1145/2034574.2034811 . Проверено 17 апреля 2023 г.

[4] «Проект F*» . Майкрософт . Проверено 20 апреля 2023 г.

[5] «fstar.exe больше нельзя собирать на F# как исполняемый файл .NET #2512» . Гитхаб . Проверено 17 апреля 2023 г.

[6] «Рассмотрите возможность исключения требования о том, что код F* должен быть действительным F# #1737» . Гитхаб . Проверено 17 апреля 2023 г.

[:0-7] Перейти обратно: ^а ^б Свами, Нихил; Мартинес, Гвидо; Растоги, Асим (14 января 2024 г.). Доказательство-ориентированное программирование на F* (PDF) .

[1]

[2]

[3]

[4]

[5]

[6]

[7]