Correctness of monadic state: an imperative call-by-need calculus

The extension of Haskell with a built-in state monad combines mathematical elegance with operational efficiency: ¿Semantically, at the source language level, constructs that act on the state are viewed as functions that pass an explicit store data structure around. ¿Operationally, at the implementation level, constructs that act on the state are viewed as statements whose evaluation has the side-effect of updating the implicit global store in …