Algebraic Identities for Program Calculation
Richard S. Bird · The Computer Journal · 1989
To calculate a program means to derive it from a suitable specification by a process of equational reasoning. We describe a number of basic algebraic identities that turn out to be extremely useful in this task. These identities express relationship between the higher-order functions commonly encountered in functional programming. The idea of program calculation is illustrated with two non-trivial examples.