Quicksort

Shin-Cheng Mu and Tsung-Ju Chiang. In Functional and Logic Programming (FLOPS), Keisuke Nakano and Konstantinos Sagonas, editors, pp. 124-138. April 2020.
[PDF |Agda Proofs]