Alasdair Armstrong, Victor B. F. Gomes, Georg Struth: Algebras for Program Correctness in Isabelle/HOL. RAMiCS 2014: 49-64