欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
F*
来自开放百科 - 灰狐
(版本间的差异)
小 (→图集) |
小 (→项目) |
||
第17行: | 第17行: | ||
==项目== | ==项目== | ||
+ | *[https://github.com/project-everest/hacl-star HACL*] a formally verified cryptographic library(形式化验证密码学库)written in F* | ||
==图集== | ==图集== |
2022年2月14日 (一) 09:07的版本
您可以在Wikipedia上了解到此条目的英文信息 F* Thanks, Wikipedia. |
F*
目录 |
简介
F*: A Proof-oriented Programming Language, Apache License 2.0.
F*(F star)是一个由微软研究院和 INRIA 主导开发的、基于ML的依赖类型函数式程序语言,主要用于程序的形式化验证。
F* 的类型检查器通过检查手写的证明和SMT自动求解来确保程序符合规范。
功能
指南
项目
- HACL* a formally verified cryptographic library(形式化验证密码学库)written in F*
图集
链接
分享您的观点