lvc:LVC验证的编译器 源码

LVC编译器项目 LVC代表线性验证编译器。 编译器基于线性一阶语言IL [1,2]。 该项目的目标是表明功能性SSA,即使用功能性样式词法变量绑定为静态单一分配(SSA)提供了可行的语义基础。 CoqDoc文档可。 依存关系 辅酶Q 来源使用Coq版本8.7.2(2018年3月)进行编译。 其他版本可能会起作用。 OCaml (包括ocamlbuild) 源代码使用ocaml 4.04.2版进行编译,其他版本也可以使用。 OCaml应该包括ocamlbuild。 门希尔 解析器生成器主要与ocamlyacc兼容(但更能解释冲突): ://gallium.inria.fr/~fpo