Declarative pearl: deriving monadic quicksort

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