[TYPES] How fast is the fastest sorting program in type theories?

[Yong Luo]

Dear all,

I would like to know the complexity of Quicksort in type theories.

According to private conversation, the complexity of Quicksort in type
theories is: Cubic. But I am not sure whether it is a correct analysis.

I have implemented a type theory with pattern matching. The complexity of
Quicksort is O(n log n) in the best case (see the following link for
details).
 http://www.cs.kent.ac.uk/people/staff/yl41/TPF.htm

The complexity of Quicksort might be different for different
implementations. I would like to collect all the results and make a
comparison.

Thank you,

Yong
==============================
Dr. Yong Luo
Computing Laboratory
University of Kent