文件名称：certicoq：Gallina编写的经过验证的Gallina编译器
文件大小：1.82MB
文件格式：ZIP
更新时间：2024-02-21 07:41:55
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/包含胶水代