The Coq mailing list

[<hugoccomp AT gmail.com>]

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? As in, other algorithms formalized reusing the
framework, or work on automatizing parts of it (automatic creation of a
fixpoint equation for a function defined with Program Fixpoint, for example, i
bet that would be useful for a lot of people). For example, what other sorting
algorithms do we have complexity proofs for? (i do realize that quicksort is
one of the few interesting ones in this class because of its notable average-
case, compared to, say, mergesort and heapsort, which are all the same big-O
complexity regardless of the input distribution)


(Disclaimer: I am a mere undergrad student; this area of work struck me as
simultaneously simple enough to be accessible even for someone such as myself,
and unexplored enough to be exciting. Just exactly how much unexplored is what
i want to know... (i am still impressed that a well-studied subject such as
quicksort's average case can be relevant to a '08 paper))