State

Declarative pearl: deriving monadic quicksort

February 20, 2020 December 4, 2020 / Monad, Non-determinism, Program Derivation, Quicksort, State

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]

Deriving Monadic Programs

December 2, 2019 December 2, 2019 / Backtracking, Effect, Galois Connection, Monad, n-Queens, Non-determinism, Program Derivation, Relation, State

I started to take an interest in reasoning and derivation of monadic programs around 2016-17. Several years having passed, I collaborated with many nice people, managed to get some results published, failed to publish some stuffs I personally like, and am still working on some interesting tiny problems. This post summaries what was done, and what remains to be done.