Contribution: QuicksortComplexity
Proofs of Quicksort's worst- and average-case complexity
Authors
- Eelis
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.
Keywords
quicksort, complexity, average case
Available files
- indices.html
- qs_det_parts.html
- ne_tree_monad.html
- list_length_expec.html
- util.html
- qs_cmp_prob.html
- qs_cases.html
- qs_nondet_avg_complexity.html
- fix_measure_utils.html
- vec.html
- qs_correct.html
- skip_list.html
- ne_list.html
- monoid_monad_trans.html
- monads.html
- insertion_sort.html
- ne_tree.html
- U.html
- list_utils.html
- qs_CM_U_expec_cost_eq.html
- harmonic.html
- sort_order.html
- qs_definitions.html
- monoid_tree_monad.html
- qs_det_avg_complexity.html
- expec.html
- qs_sound_cmps.html
- qs_worst.html
- sums_and_averages.html
- qs_case_split.html
- nat_below.html
- monoid_expec.html
- arith_lems.html
- qs_parts.html
- NDP.html
- nat_seqs.html