Output details
11 - Computer Science and Informatics
University of Edinburgh
A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
<12> Originality: One of the few papers in interactive theorem proving to consider verification of non-functional properties of formalised algorithms: here a classic result in algorithmic complexity.
Significance: Follows a textbook proof, involving a tricky technical lemma, requiring formal justification. Towards the main result, the paper develops a general framework for expressing worst- and average-case algorithmic complexity in type theory, using operation-counting monads for probabilistic non-determinism, and a theory of expectation for such computations. Received informal Best Paper award from the editors (private communication), based on overall review scores.
Rigour: Fully formalised and machine-checked in the Coq theorem prover.