Verifying stateful programs with substructural state and hoare types
Johannes Borgström, Juan Chen, Nikhil Swamy · 2011
A variety of techniques have been proposed to verify stateful functional programs by developing Hoare logics for the state monad. For better automation, we explore a different point in the design space: we propose using affine types to model state, while relying on refinement type checking to prove assertion safety.