文件名称：event-struct:事件结构的机械化理论
文件大小：36KB
文件格式：ZIP
更新时间：2024-04-09 17:21:56
Coq
事件结构的机械化理论 一个Coq形式化的事件结构理论库，适用于并发语义。包括主要事件结构和操作性小步语义的渐进式构造理论。 文件说明 所有文件都包含对其内容的更详细描述。 utilities.v 实用引理和策略。包括用于ssreflect的lia类似物ssrnatlia ，由Assia Mahboubi从提取。 inhtype.v 居住类型的接口，即具有一个杰出居民的类型。 wftype.v 具有部分依据的类型的接口。 ident.v 可用作标识符的类型的接口。我们需要以下属性。 ident0第一个标识符。 fresh : T -> T返回新鲜标识符的函数。 forall x, x < fresh x新鲜公理。我们要求<必须有充分的依据。 relations.v 可计算的，传递式关闭良好关系的理论。 eventstructure.v 有限素数事件结构理论。 transitionsys
【文件预览】：
event-struct-master
----pomset.v(5KB)
----_CoqProject(445B)
----.github()
--------workflows()
----monoid.v(6KB)
----utilities.v(13KB)
----prime_eventstruct.v(6KB)
----Styleguide.md(6KB)
----eventstructure.v(19KB)
----dependency-graph.sh(1KB)
----inhtype.v(2KB)
----transitionsystem.v(10KB)
----relations.v(7KB)
----LICENSE(1KB)
----README.md(1KB)
----Makefile(726B)
----regmachine.v(9KB)
----CONTRIBUTORS.md(206B)
----.gitignore(152B)
----ident.v(5KB)
----wftype.v(3KB)
----coq-event-struct.opam(1KB)