Yu-Hsi Chianga, Shin-Cheng Mu. *Journal of Logical and Algebraic Methods in Programming*, in press.

[Paper(doi:10.1016/j.jlamp.2015.12.003) | Code]

Many programming tasks can be specified as optimisation problems in which a relation is used to generate all possible solutions, from which we wish to choose an optimal one. A relational operator “shrink”, developed by José N. Oliveira, is particularly suitable for constructing greedy algorithms from such specifications. Meanwhile, it has become standard in many sub-fields in programming language that proofs must be machine-verified. This tutorial leads the readers through the development of algebraic derivations of three greedy algorithms, one fold-based and two unfold-based, using AoPA, a library designed for machine-verified relational program calculation.