F*

F*
	File:Fstar-official-logo-2015.png
编程范型	多范式：函数式、指令式、面向对象、元编程、并发编程
設計者	微软研究院、INRIA
当前版本	Template:Software version
型態系統	静态类型、强类型、类型推断
操作系统	Linux, macOS, Windows
許可證	Apache许可证
文件扩展名	.fst
網站	https://fstar-lang.org/
受影响于
	F#、OCaml、Standard ML、Coq、脚本错误：没有“ilh”这个模块。、脚本错误：没有“ilh”这个模块。

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上^[1]。

引用[编辑]

package.lua第80行Lua错误：module 'Module:Navbar/configuration' not found