# Program Derivation

## Declarative pearl: deriving monadic 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]

## How to Compute Fibonacci Numbers?

Some inductive proofs and some light program derivation about Fibonacci numbers. If you think the fastest way to compute Fibonacci numbers is by a closed-form formula, you should read on!

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.

## Calculating a backtracking algorithm: an exercise in monadic program derivation

Shin-Cheng Mu. Tech. Report TR-IIS-19-003, Institute of Information Science, Academia Sinica, June 2019.
[PDF]

## Equational reasoning for non-determinism monad: the case of Spark aggregation

Shin-Cheng Mu. Tech. Report TR-IIS-19-002, Institute of Information Science, Academia Sinica, June 2019.
[PDF]

## Queueing and glueing for optimal partitioning

Shin-Cheng Mu, Yu-Hsi Chiang, and Yu-Han Lyu. In the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Eijiro Sumii, editor, pages 158-167. ACM Press, Sep. 2016.
[Paper | Code]

## Formal derivation of greedy algorithms from relational specifications: a tutorial

Yu-Hsi Chiang, Shin-Cheng Mu. Journal of Logical and Algebraic Methods in Programming, 85(5), Part 2, pp 879-905, August 2016.
[Paper(doi:10.1016/j.jlamp.2015.12.003) | Code]

## Calculating a linear-time solution to the densest segment problem

Sharon Curtis and Shin-Cheng Mu. Calculating a linear-time solution to the densest segment problem. Journal of Functional Programming, Vol. 25, 2015.
[Paper (doi: 10.1017/S095679681500026X)| Supplementary Proofs | Code]

The problem of finding a densest segment of a list is similar to the well-known maximum segment sum problem, but its solution is surprisingly challenging. We give a general specification of such problems, and formally develop a linear-time online solution, using a sliding window style algorithm. The development highlights some elegant properties of densities, involving partitions that are decreasing and all right-skew.

## Programming from Galois connections

Shin-Cheng Mu and José Nuno Oliveira. Programming from Galois connections. In the Journal of Logic and Algebraic Programming , Vol 81(6), pages 680–704, August 2012.
[PDF]

## Calculating Programs from Galois Connections

One is often amazed that, once two functions are identified as a Galois connection, a long list of nice and often useful properties follow from one concise, elegant defining equation. But how does one construct a program from a specification given as a Galois connection?