Proofs by equational reasoning

Collecting some material on proofs that are chains of equations (or implications and rewriting), usually using a compact notation.

The APL school

Programming Style in APL, by Kenneth E. Iverson (1978). In particular, Chapter 5 “Proofs”.

Notation as a Tool of Thought, by Kenneth E. Iverson (1980). In particular, Chapter 4 “Identities and Proofs”.

Tests, Derivations, Proofs, by Roger K.W. Hui (2017).

The Bird-Meertens formalism

Also known as Squiggol, due to the prevailing use of symbols.

An Exploration of the Bird-Meertens Formalism, by Roland Backhouse (1988). 110 theorems in Squiggol.

Relational Catamorphisms, by R. C. Backhouse, P. J. de Bruin, G. Malcom, E. Voermans, and J. van der Woude (1991).

Calculating Compilers, by Erik Meijer (1992). For correctness proofs in compiler transformations.

Theories for Algorithm Calculation, by Johan Theodoor Jeuring (1993).

Algebra of Programming, by Richard Bird and Oege de Moor (1997).

Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, by Erik Meijer, Maarten Fokkinga, and Ross Paterson (2000).

Exercises in Quantifier Manipulation, by Roland Backhouse (2006). Good intro.

On a Basic Property for the Longest Prefix Problem, by Shin-Cheng Mu (2009). See also his other publications.

The School of Squiggol: A History of the Bird–Meertens Formalism, by Jeremy Gibbons (2019).

Haskell

Just do It: Simple Monadic Equational Reasoning, by Jeremy Gibbons and Ralf Hinze (2011).

Thinking Functionally with Haskell, Richard Bird (2014).

Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell), by Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, and Graham Hutton (2018).

This style of proofs is also popular in Agda and Lean.