package coq-quicksort-complexity
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Proofs of Quicksort's worst- and average-case complexity
Install
Dune Dependency
Authors
Maintainers
Sources
v8.9.0-1.tar.gz
md5=9fa8d740e916e98f6f46d8dc7c2e7f30
Description
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.
Most of the development is documented in the TYPES 2008 paper "A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq", available at the homepage.
On This Page