F* (programming language) (original) (raw)

dbo:abstract

F* (pronounced F star) is a functional programming language inspired by ML and aimed at program verification. Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs.Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript. The latest version of F* is written entirely in a common subset of F* and F#, and bootstraps in both OCaml and F#. It is open source (under the Apache License 2.0) and is under active development on GitHub. (en)
F* (F スター) はプログラム検証を目的とした、MLに影響を受けた関数型プログラミング言語である。型システムには依存型、モナディックエフェクトの要素が組み込まれており、それによりプログラムの詳細な仕様を型で表現することができる。F*の型検査機はプログラムが仕様を満たすことをSMT solvingと手動証明を組み合わせて証明する。F*のプログラムはOCaml、F#、C言語に変換され実行される。 (ja)
F * (произносится как F star) — функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ. Его система типов включает в себя зависимые типы, монадические эффекты и . Этих выразительных средств достаточно, чтобы задавать точные спецификации для программ, включая описания функциональной корректности и свойств безопасности. Механизм проверки типов в F* позволяет доказывать, что программы соответствуют их спецификациям. Это делается с использованием комбинации SMT-решателя и ручных доказательств. Программы, написанные на F*, могут быть странслированы в OCaml, F# и C для дальнейшей компиляции и выполнения. Предыдущие версии F* также можно было транслировать в JavaScript. Последняя версия F* написана полностью на общем подмножестве F* и F# и может быть запущена как с использованием OCaml, так и с использованием F#. Исходный код языка открыт под лицензией Apache 2.0 и активно разрабатывается на GitHub. (ru)
F*（读作“F star”）是一个由微软研究院和INRIA主导开发的、基于ML的依赖类型函数式程序语言，主要用于程序的形式化验证。 F*的类型系统十分丰富，支持依赖类型、单子化效用（monadic effects）和细化类型（refinement types）。这使其能够准确地用于表述程序的形式化规范，包括功能正确性和安全性。F*的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。使用F*书写的程序可被编译到OCaml、F#或C加以执行。早期版本的F*亦支持编译到JavaScript。 F*语言本身使用F*和F#实现，并可从OCaml或F#引导。它的源码使用Apache协议授权，目前托管在GitHub上。 (zh)

dbo:thumbnail

wiki-commons:Special:FilePath/Fstar-official-logo-2015.png?width=300

dbo:wikiPageExternalLink

dbo:wikiPageID

38420593 (xsd:integer)

dbo:wikiPageLength

4714 (xsd:nonNegativeInteger)

dbo:wikiPageRevisionID

1119642763 (xsd:integer)

dbo:wikiPageWikiLink

dbp:designers

Microsoft Research and Inria (en)

dbp:fileExt

.fst (en)

dbp:influencedBy

dbp:latestReleaseVersion

https://github.com/FStarLang/FStar

dbp:license

dbr:Apache_License_2.0

dbp:logo

Fstar-official-logo-2015.png (en)

dbp:logoSize

128 (xsd:integer)

dbp:name

F* (en)

https://www.fstar-lang.org/

dbp:wikiPageUsesTemplate

dct:subject

gold:hypernym

dbr:Programming

rdf:type

rdfs:comment

F* (F スター) はプログラム検証を目的とした、MLに影響を受けた関数型プログラミング言語である。型システムには依存型、モナディックエフェクトの要素が組み込まれており、それによりプログラムの詳細な仕様を型で表現することができる。F*の型検査機はプログラムが仕様を満たすことをSMT solvingと手動証明を組み合わせて証明する。F*のプログラムはOCaml、F#、C言語に変換され実行される。 (ja)
F*（读作“F star”）是一个由微软研究院和INRIA主导开发的、基于ML的依赖类型函数式程序语言，主要用于程序的形式化验证。 F*的类型系统十分丰富，支持依赖类型、单子化效用（monadic effects）和细化类型（refinement types）。这使其能够准确地用于表述程序的形式化规范，包括功能正确性和安全性。F*的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。使用F*书写的程序可被编译到OCaml、F#或C加以执行。早期版本的F*亦支持编译到JavaScript。 F*语言本身使用F*和F#实现，并可从OCaml或F#引导。它的源码使用Apache协议授权，目前托管在GitHub上。 (zh)
F* (pronounced F star) is a functional programming language inspired by ML and aimed at program verification. Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs.Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript. (en)
F * (произносится как F star) — функциональный язык программирования, основанный на ML и ориентированный на формальную верификацию разрабатываемых на нём программ. Его система типов включает в себя зависимые типы, монадические эффекты и . Этих выразительных средств достаточно, чтобы задавать точные спецификации для программ, включая описания функциональной корректности и свойств безопасности. Механизм проверки типов в F* позволяет доказывать, что программы соответствуют их спецификациям. Это делается с использованием комбинации SMT-решателя и ручных доказательств. Программы, написанные на F*, могут быть странслированы в OCaml, F# и C для дальнейшей компиляции и выполнения. Предыдущие версии F* также можно было транслировать в JavaScript. (ru)

rdfs:label