You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Edinburgh » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Edinburgh

Return to search Previous output Next output

Output 22 of 401 in the submission

Output title

A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq

Type

E - Conference contribution

DOI

10.1007/978-3-642-02444-3_16

Name of conference/published proceedings

Types for Proofs and Programs : International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers

Volume number

5497

Issue number

First page of article

256

ISSN of proceedings

0302-9743

Year of publication

2009

URL

http://dx.doi.org/10.1007/978-3-642-02444-3_16

Number of additional authors

Additional information

<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.

Interdisciplinary

Cross-referral requested

Research group

F - Laboratory for Foundations of Computer Science

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract