热门问题
时间线
聊天
视角

F*

来自维基百科,自由的百科全书

F*
Remove ads

F*(读作“F star”)是一个由微软研究院INRIA主导开发的、基于ML依赖类型函数式程序语言,主要用于程序的形式化验证。

事实速览 编程范型, 設計者 ...

F*的类型系统十分丰富,支持依赖类型、单子化效用(monadic effects)和细化类型(refinement types)。这使其能够准确地用于表述程序的形式化规范,包括功能正确性和安全性。 F*的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。

使用F*书写的程序可被编译到OCamlF#C加以执行。早期版本的F*亦支持编译到JavaScript。

F*语言本身使用F*和F#实现,并可从OCamlF#引导。它的源码使用Apache协议授权,目前托管在GitHub[2]

Remove ads

引用

外部链接

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads