The Coq mailing list

[Eelis van der Weegen <eelis AT eelis.net>]

On 2012-05-16 04:42, 
hugoccomp AT gmail.com
 wrote:
> Hi club!
>
> Recently I've read Mr. Eelis's work on a framework for complexity analysis of
> algorithms, with Quicksort as a case study (you may find his paper on this at
> http://weegen.home.xs4all.nl/eelis/research/quicksort/, and the updated code
> is available in Coq's user contributions section).
>
> Does anyone know if there have been any further developments in that area
> beyond that first article?

Apart from committing a separate proof for /deterministic/ Quicksort's 
average case complexity, I have not done any follow-up work using the 
development, nor am I aware of anybody else using it for anything.

Cheers,

Eelis