F* - Язык_программирования

software.wikisort.org - Язык_программирования

F * (произносится как F star) — функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ.

F*

Класс языка	мультипарадигменный: функциональное, объектно-ориентированное, обобщённое, императивное программирование
Автор	Microsoft Research и INRIA[1]
Разработчик	Microsoft Research[2] и INRIA
Система типов	строгая, статическая, с выводом типов, с зависимыми типами
Испытал влияние	Coq, Dafny^[en], F#, Lean, OCaml, Standard ML
Лицензия	Apache Software License
Сайт	fstar-lang.org
ОС	Кроссплатформенное программное обеспечение (Linux, macOS, Windows)

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

Последняя версия F* написана полностью на общем подмножестве F* и F# и может быть запущена как с использованием OCaml, так и с использованием F#. Исходный код языка открыт под лицензией Apache 2.0 и активно разрабатывается на GitHub[3].

Литература

(2017) «Dijkstra Monads for Free». 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
(2016) «Dependent Types and Multi-Monadic Effects in F*». 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Ссылки

Microsoft Research (MSR)

Основные
проекты

Языки программирования и компиляторы	Bartok Bosque Cω F* Lean P Phoenix Polyphonic C# Sing# Spec#
Распределённые вычисления/Грид	Bigtop Gridline BitVault Orleans
Интернет и сети	AjaxView Avalanche Conference XP Gazelle HoneyMonkey Penny Black Wallop WikiBhasha
Другое	Cognitive Toolkit IllumiRoom Image Composite Editor MyLifeBits LiveStation SLAM Terminator WorldWide Telescope PhotoDNA Z3 Theorem Prover Courier
Операционные системы	Barrelfish HomeOS Midori Singularity Verve
API	Joins Accelerator Dryad SXM
Выпущено в качестве отдельного продукта	C# Comic Chat Detours F# Боковая панель Windows PixelSense (TouchLight) SenseCam ClearType Group Shot Allegiance TrueSkill Songsmith Xbox Kinect

MSR Labs

Live Labs^[en]

Актуальные	Pivot Seadragon Deep Zoom DeepZoomPix
Прекращённые	Deepfish Listas Live Clipboard Photosynth Volta

FUSE Labs^[en]

Bing Twitter
Docs.com
Kodu

Другие подразделения

Academic Search
adCenter Labs
Office Labs

Категория

Свободное и открытое программное обеспечение Microsoft

Общая информация

Microsoft и открытое программное обеспечение^[en]
Shared Source Initiative

Программное
обеспечение

Приложения	Atom Conference XP Диспетчер файлов Open Live Writer PowerToys for Windows 10 Калькулятор (Windows) Windows Console Windows Package Manager Windows Terminal WorldWide Telescope XML Notepad
Игры	Allegiance
Языки программирования	Bosque C# Dafny F# F* GW-BASIC IronPython IronRuby Lean P PowerShell Q# R Open Small Basic TypeScript Visual Basic .NET
Фреймворки и средства разработки	.NET Bio .NET .NET Framework .NET Gadgeteer .NET Micro Framework ADO.NET Entity Framework AirSim Apache Helix ASP.NET ASP.NET AJAX ASP.NET Core ASP.NET MVC ASP.NET Razor ASP.NET Web Forms Blazor C++/WinRT ChakraCore CLR Profiler DiskSpd Dryad Dynamic Language Runtime Electron Managed Extensibility Framework Microsoft Automatic Graph Layout Microsoft C++ Standard Library Microsoft Cognitive Toolkit Microsoft Detours Microsoft Enterprise Library Microsoft SEAL ML.NET mod_mono Mono MonoDevelop MSBuild npm NuGet Open Management Infrastructure ONNX Orleans ProcDump Python Tools for Visual Studio R Tools for Visual Studio Roslyn Sandcastle SignalR StyleCop SVNBridge T2 Temporal Prover Text Template Transformation Toolkit TLA⁺ U-Prove vcpkg Virtual File System for Git Visual Studio Code Voldemort Vowpal Wabbit Windows Communication Foundation Windows Driver Frameworks Windows Forms Windows Presentation Foundation Windows Template Library Windows UI Library WinJS WinObjC WiX XSP xUnit.net Z3 Theorem Prover
Операционные системы	MS-DOS Barrelfish
Прочее	ChronoZoom Project Mu SILK TLAPS TPM 2.0 Reference Implementation WikiBhasha

Лицензии

Microsoft Public License
Microsoft Reciprocal License

Связанные
темы

.NET Foundation
F Sharp Software Foundation
Microsoft Open Specification Promise
Outercurve Foundation

Категория

Примечания

Microsoft Research Inria Joint Centre (неопр.). MSR-INRIA. Дата обращения: 28 мая 2020. Архивировано 21 мая 2020 года.
https://www.fstar-lang.org/#people
FStarLang/FStar (неопр.). GitHub. Дата обращения: 28 мая 2020. Архивировано 10 июля 2020 года.

Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.org внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2025
WikiSort.org - проект по пересортировке и дополнению контента Википедии