stablesort
stablesort copied to clipboard
pi8027
Stable sort algorithms and their stability proofs in Coq
"Usual" stability is equivalent to "lexicographic" stability
because calling `native_compute` eventually makes `native_compute` itself slower: coq/coq#15528. To improve the situation, `benchmark.v` (currently written in Elpi) has to be reimplemented as an external tool (e.g., written as a...
It is intended to serve just as an example of our verification technique and is not considered part of the stable sort library. This example corresponds to Sections 4.1 and...