This paper proposes new derivations of three well-known sorting algorithms, in their functional formulation. The approach we use is based on three main ingredients: first, the algorithms are derived from a simpler algorithm, i.e. the specification is already a solution to the problem (in this sense our derivations are program transformations). Secondly, a mixture of inductive and coinductive arguments are used in a uniform, algebraic style in our reasoning. Finally, the approach uses structural invariants so as to strengthen the equational reasoning with logical arguments that cannot be captured in the algebraic framework.

Technical Report