back to index

Mergesort stability proof

This archive contains two formal proofs of correctness for a specific mergesort function. The proofs are written for the ACL2 theorem prover.

Not all versions of mergesort are stable, and while proofs that mergesort yields an ordered permutation of its input can be easily found, I could not locate an ACL2 stability proof. The two proofs are intended to fill that gap.

mergesort-stable-acl2.tar.gz.


Contact:

Stefan Krah <website @ bytereef.org>