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

DOI10.1007/978-3-642-02444-3_16zbMath1246.68201OpenAlexW1537838026MaRDI QIDQ3638257

James McKinna, Eelis van der Weegen

Publication date: 2 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.180.4337

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Searching and sorting (68P10)

Related Items (2)

Verified analysis of random binary tree structures ⋮ A Coq Library for Internal Verification of Running-Times

Uses Software

• Coq
• Quicksort

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The analysis of Quicksort programs
• Subset Coercions in Coq
• Proofs of Randomized Algorithms in Coq

This page was built for publication: A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq