IMP2 β Simple Program Verification in Isabelle/HOL by Peter Lammich π and Simon Wimmer π Jan 15
Monadification, Memoization and Dynamic Programming by Simon Wimmer π, Shuwei Hu π§ and Tobias Nipkow π May 22