文件名称：mergesort:归并排序正确性证明
文件大小：350KB
文件格式：ZIP
更新时间：2024-06-24 15:07:44
proof sort agda correctness sort-correctness-proof
归并排序 （相当）无痛依赖类型编程的案例：Agda 中完全认证的归并排序 Agda 中的合并排序正确性证明 我们在 Agda 中展示了一个经过完全认证的合并排序版本。 它的特点是：终止的句法保证（即不需要明确的终止证明），没有证明成本来确保输出被排序，并且几乎免费证明输出是输入的排列。 文档文件 sblp2014_submission_31.pdf - 提交给论文 源文件 Nat.agda - 第 2 节 - 有上限的自然数 Snat.agda - 第 2 节 - Agda 的大小类型介绍 MergeSort.agda - 第 2 节 - 使用 Sized Types 的终止检查合并排序 MergeSort3.agda - 第 3 节 - 合并排序算法针对列表排序规范的正确性证明 Permutation.agda - 第 3 节 - 排列相关的东西 MergeSort4.agda - 第
【文件预览】：
mergesort-master
----SNat.agda(538B)
----.gitignore(16B)
----MergeSort3.agda(3KB)
----MergeSort4.agda(4KB)
----.travis.yml(491B)
----MergeSort3Perm.agda(2KB)
----sblp2014_submission_31.pdf(343KB)
----README.md(2KB)
----MergeSort.agda(2KB)
----Permutation.agda(11KB)
----Nat.agda(741B)