SemanticsWithApplications:Agda中的形式语义

【文件属性】：
文件名称：SemanticsWithApplications:Agda中的形式语义
文件大小：43KB
文件格式：ZIP
更新时间：2021-05-24 08:38:33
Agda Agda形式化以及Nielson和Nielson 各个部分的证明及其。 该代码已使用和0.9版进行了检查。 1.一般说明 我在这里做什么 我涵盖了本书的第1、2、3和6章，因此，操作语义和公理语义各部分，省略了指称语义和静态分析。 我从书中获得了定义，将其移植到了Agda，同时包括了书中所掩盖的缺失部分（如变量绑定），还证明了每一章的主要结果。 我没有使用书中的证明作为参考就做了所有的Agda证明。 结果是存在一些差异，但差异不大。 这些定理很简单，而且受足够的约束，因此证明遵循基本相同的蓝图。 我跳过了指称语义，因为在Agda中忠实地处理它可能需要其他先进的机器，例如协和和偏分单子，而我对此经验很少。 我为什么做 首先，机器检查的证明比人类检查的正式证明更值得信赖。 尽管可以通过底层基础结构中的错误来破坏它们，但此类事故的可能性比普遍存在的人为错误小，并且与人为错误不同，它们在修正

【文件预览】：
SemanticsWithApplications-master
----.gitignore(18B)
----README.md(8KB)
----Basic()
--------EqvSemantics.agda(3KB)
--------SmallStep.agda(9KB)
--------Axiomatic()
--------AST.agda(4KB)
--------Compiler()
--------BigStep.agda(10KB)
----Utils()
--------Monoid.agda(634B)
--------NatOrdLemmas.agda(2KB)
--------Decidable.agda(5KB)
----LICENSE.txt(1KB)
----Extended()
--------FunRetRec.agda(19KB)