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