mergesort:归并排序正确性证明

归并排序 （相当）无痛依赖类型编程的案例：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 - 第