【文件属性】:
文件名称:certicoq:Gallina编写的经过验证的Gallina编译器
文件大小:1.82MB
文件格式:ZIP
更新时间:2021-01-31 13:55:15
compiler coq formal-verification gallina CompilerCoq
切尔蒂科克
总览
CertiCoq是用于Coal的规范语言Gallina的编译器。 CertiCoq面向Clight,它是C语言的子集,可以用任何C编译器(包括经过验证的编译器)进行编译。
CertiCoq编译器的大部分已经过验证,而其他部分正在验证中。
文献资料
有使用将Gallina编译为C以及与生成的C代码进行接口的说明。
您还可以和找到一些演示。
安装说明
有关安装说明,请参见 。
现有成员
Andrew Appel,Yannick Forster,Anvay Grover,Joomy Korkut,John Li,Zoe Paraskevopoulou和Matthieu Sozeau。
过去的成员和贡献者
Abhishek Anand,Greg Morrisett,Randy Pollack,Olivier Savary Belanger,Matthew Weaver
执照
CertiCoq是开放源代码,并根据分发。
目录结构
theories/包含编译器的源代码
plugin/包含用于Coq的CertiCoq插件
benchmarks/包含基准套件
glue/包含胶水代