Skip to content
Proofs of Quicksort's worst- and average-case complexity
Coq Other
  1. Coq 99.7%
  2. Other 0.3%
Branch: master
Clone or download


Travis DOI

The development contains:

  • a set of monads and monad transformers for measuring a (possibly nondeterministic) algorithm's use of designated operations;
  • monadically expressed deterministic and nondeterministic implementations of Quicksort;
  • proofs of these implementations' worst- and average case complexity.

More details about the project can be found in the paper A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq.


  • Author(s):
    • Eelis van der Weegen (initial)
  • License: Public Domain
  • Compatible Coq versions: Coq 8.8 or later (use releases for other Coq versions)
  • Additional dependencies: none

Building and installation instructions

The easiest way to install the latest released version is via OPAM:

opam repo add coq-released
opam install coq-quicksort-complexity

To instead build and install manually, do:

git clone
cd quicksort-complexity
make   # or make -j <number-of-cores-on-your-machine>
make install

After installation, the included modules are available under the QuicksortComplexity namespace.

You can’t perform that action at this time.