The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

On Wed, 3 Aug 2005, Stefan Karrmann wrote:

> Apologies for answering myself here.
>
> > [...]
> > functions which are defined and accepted in Coq terminates. Can the system
> > check space and time upper bounds, i.e. O(f) bounds?

We did some experiment in an old version of Coq some years a ago along 
your line to compute worse case complexity. We even built a tool for a 
restricted subset of function that was semi-automatically producing the 
transformed function. We proved for example that isort was quadratic.
So it works

--
Laurent Théry