for the few of us.

Given an interpreter of a small language, derive a virtual machine and a corresponding compiler

S-C. Mu. Maximum segment sum is back: deriving algorithms for two segment problems with bounded lengths. In Partial Evaluation and Program Manipulation (PEPM ‘08), pp 31-39. January 2008.
[PDF] [GZipped Postscript]

To practise using the Logic.ChainReasoning module in Agda, Josh proved the foldr-fusion theorem, and I thought it would be an small exercise over the weekend to start off where he finished…