文件名称：semantics:Coq中语义样式的调查，从自然语义到结构化操作，公理和指称语义，再到抽象解释[maintainer = @ k4rtik]
文件大小：57KB
文件格式：ZIP
更新时间：2024-06-17 10:12:22
coq programming-language-semantics Coq
语义学 这是一个编程语言语义样式的调查，它是一种编程语言的微型示例，包括它们在Coq中的编码，不同样式的等价性证明以及从公理语义或抽象解释获得的工具的健全性证明。 这些工具可以在Coq内运行，因此可以通过反射进行验证，并且由于使用了由模块的字符串类型参数化的函子，因此还可以提取代码并将其连接到基于yacc的解析器。 Coq中还提供了一个手写的解析器，但是没有相关的证明。 元 作者： 伊夫·贝托（Yves Bertot）（初始） Coq社区维护者： Kartik Singhal（ ） 执照： 兼容的Coq版本：8.10或更高版本 其他依赖项：无 Coq名称空间： Semantics 相关出版物： doi： 建造和安装说明 安装最新发布的语义版本的最简单方法是通过 ： opam repo add coq-released https://coq.inria.fr/opam/rel
【文件预览】：
semantics-master
----example2.v(1KB)
----tail_sqrt.v(300B)
----ex.lil(60B)
----_CoqProject(193B)
----context_sqrt.v(176B)
----denot.v(4KB)
----.github()
--------workflows()
----little_w_string.v(5KB)
----parser.v(18KB)
----fact.lil(169B)
----coq-semantics.opam(2KB)
----little.v(13KB)
----constructs.v(2KB)
----str_little.ml(1KB)
----sqrt.lil(132B)
----syntax.v(2KB)
----example.v(3KB)
----llex.mll(757B)
----LICENSE(1KB)
----parse_little.mly(3KB)
----ex_int2.lil(89B)
----README.md(6KB)
----Makefile(226B)
----extract_interpret.v(468B)
----ex_i.v(514B)
----ex_int3.lil(260B)
----abstract_i.v(69KB)
----axiom.v(11KB)
----little.ml(6KB)
----.gitignore(392B)
----function_cpo.v(14KB)
----Makefile.coq.local(570B)
----ex_int.lil(91B)
----fact_err.lil(167B)
----intervals.v(39KB)
----meta.yml(5KB)