F*

维基百科,自由的百科全书
跳到导航 跳到搜索
F*
Fstar-official-logo-2015.png
编程范型多范式函数式指令式面向对象元编程并发编程
設計者微软研究院、MSR-INRIA、INRIA
實作者微软研究院、MSR-INRIA、法国国家信息与自动化研究所
穩定版本
0.9.7.0-alpha1
( 2019年6月26日 (2019-06-26)
型態系統静态类型强类型类型推断
作業系統跨平台.NET框架
許可證Apache许可证
文件扩展名.fst
網站https://fstar-lang.org/
啟發語言
F♯OCamlStandard ML、Fine、F7、F5、FX、HTT、Trellys、Zombie、Dafny

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 上。

外部链接[编辑]