[TYPES] Is Quick Sort slower than Insertion Sort in type theories?

[Yong Luo]

Dear all,

I posted an email about Quick Sort few days ago. Thank you for your reply.

Insertion Sort is primitive recursion, so it is easy to program it in type
theories and the average complexity is O(n^2).

Quick Sort is not primitive recursion, so there are proofs in the program
when it is programmed in type theories. I am told that the average
complexity "might" be O(n^3), or might be worse. Please let me know if you
know of any work on this.

Regards,

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