| From: | Dann Corbit <DCorbit(at)connx(dot)com> |
|---|---|
| To: | Dann Corbit <DCorbit(at)connx(dot)com>, 'Greg Stark' <stark(at)mit(dot)edu> |
| Cc: | Bruce Momjian <bruce(at)momjian(dot)us>, Peter Geoghegan <peter(dot)geoghegan86(at)gmail(dot)com>, Robert Haas <robertmhaas(at)gmail(dot)com>, Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)us>, PG Hackers <pgsql-hackers(at)postgresql(dot)org> |
| Subject: | Re: Why do we still perform a check for pre-sorted input within qsort variants? |
| Date: | 2013-03-09 21:10:33 |
| Message-ID: | 87F42982BF2B434F831FCEF4C45FC33E5BD36A05@EXCHANGE.corporate.connx.com |
| Views: | Raw Message | Whole Thread | Download mbox | Resend email |
| Thread: | |
| Lists: | pgsql-hackers |
"A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq"
By Eelis van der Weegen and James McKinna
Institute for Computing and Information Sciences
Radboud University Nijmegen
Heijendaalseweg 135, 6525 AJ Nijmegen, The Netherlands
Contains a formal proof, validated by machine logic, that quicksort is quadratic in the worst case and also a formal proof of the average runtime efficiency.
| From | Date | Subject | |
|---|---|---|---|
| Next Message | Greg Stark | 2013-03-09 21:21:12 | Re: Why do we still perform a check for pre-sorted input within qsort variants? |
| Previous Message | Dann Corbit | 2013-03-09 20:52:28 | Re: Why do we still perform a check for pre-sorted input within qsort variants? |