certicoq:Gallina编写的经过验证的Gallina编译器 源码

切尔蒂科克 总览 CertiCoq是用于Coal的规范语言Gallina的编译器。 CertiCoq面向Clight,它是C语言的子集,可以用任何C编译器(包括经过验证的编译器)进行编译。 CertiCoq编译器的大部分已经过验证,而其他部分正在验证中。 文献资料 有使用将Gallina编译为C以及与生成的C代码进行接口的说明。 您还可以和找到一些演示。 安装说明 有关安装说明,请参见 。 现有成员 Andrew Appel,Yannick Forster,Anvay Grover,Joomy Korkut,John Li,Zoe Paraskevopoulou和Matthieu Soze