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

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 language | English |
---|---|

Title of host publication | Types for Proofs and Programs |

Subtitle of host publication | International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers |

Editors | Stefano Berardi, Ferruccio Damiani, Ugo de'Liguoro |

Publisher | Springer-Verlag GmbH |

Pages | 256-271 |

Number of pages | 16 |

ISBN (Electronic) | 978-3-642-02444-3 |

ISBN (Print) | 978-3-642-02443-6 |

DOIs | |

Publication status | Published - 2009 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin / Heidelberg |

Volume | 5497 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |