Towards Hoare logic for a small imperative language in Haskell

bor0.wordpress.com