A machine-checked proof of the average-case complexity of quicksort in coq

Eelis Van Der Weegen, James McKinna

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

As a case-study in machine-checked reasoning about the complexity of algorithms in type theory, we describe a proof of the average-case complexity of Quicksort in Coq. The proof attempts to follow a textbook development, at the heart of which lies a technical lemma about the behaviour of the algorithm for which the original proof only gives an intuitive justification. We introduce a general framework for algorithmic complexity in type theory, combining some existing and novel techniques: algorithms are given a shallow embedding as monadically expressed functional programs; we introduce a variety of operation-counting monads to capture worst- and average-case complexity of deterministic and nondeterministic programs, including the generalization to count in an arbitrary monoid; and we give a small theory of expectation for such non-deterministic computations, featuring both general map-fusion like results, and specific counting arguments for computing bounds. Our formalization of the average-case complexity of Quicksort includes a fully formal treatment of the 'tricky' textbook lemma, exploiting the generality of our monadic framework to support a key step in the proof, where the expected comparison count is translated into the expected length of a recorded list of all comparisons.

Original languageEnglish
Title of host publicationTypes for Proofs and Programs. TYPES 2008
PublisherSpringer
Pages256-271
Number of pages16
ISBN (Electronic)9783642024443
ISBN (Print)9783642024436
DOIs
Publication statusPublished - 2009
EventInternational Conference on Types for Proofs and Programs 2008 - Torino, Italy
Duration: 26 Mar 200829 Mar 2008

Publication series

NameLecture Notes in Computer Science
Volume5497
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Types for Proofs and Programs 2008
Abbreviated titleTYPES 2008
CountryItaly
CityTorino
Period26/03/0829/03/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A machine-checked proof of the average-case complexity of quicksort in coq'. Together they form a unique fingerprint.

  • Cite this

    Van Der Weegen, E., & McKinna, J. (2009). A machine-checked proof of the average-case complexity of quicksort in coq. In Types for Proofs and Programs. TYPES 2008 (pp. 256-271). (Lecture Notes in Computer Science; Vol. 5497). Springer. https://doi.org/10.1007/978-3-642-02444-3_16