Merge sort correctness proof in Agda
We present a version of merge sort, fully certified, in Agda. It features: syntactic warrant of termination (i.e. no need of explicit termination proof), no proof cost to ensure the output is sorted, and almost free proof that the output is a permutation of the input.
- sblp2014_submission_31.pdf - Submited paper to Lecture Notes in Computer Science, Springer
- Nat.agda - Section 2 - Natural numbers with an upper bound
- Snat.agda - Section 2 - Agda's Sized Types introduction
- MergeSort.agda - Section 2 - Merge sort with Sized Types's termination check
- MergeSort3.agda - Section 3 - Merge sort algorithm's correctness proof against list's sort specification
- Permutation.agda - Section 3 - Permutation related stuff
- MergeSort4.agda - Section 3 - Merge sort algorithm's correctness proofagainst list's sort and permutation specifications
- MergeSort3Perm.agda - Section 3 - Merge sort algorithm's correctness proof against permutation specifications, not embedding algorhitm's code within the proof as in MergeSort4 file
Agda version 2.3.2.2 Standard Library version 0.7
