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]
To demonstrate derivation of monadic programs, we present a specification of sorting using the non-determinism monad, and derive pure quicksort on lists and state-monadic quicksort on arrays. In the derivation one may switch between point-free and pointwise styles, and deploy techniques familiar to functional programmers such as pattern matching and induction on structures or on sizes. Derivation of stateful programs resembles reasoning backwards from the postcondition.
Interested paper!
I’m trying to reproduce some of the proofs. What version of Agda and the Standard Library were used for the proofs in this paper?