A Hoare Logic for the State Monad

Abstract. This pearl examines how to verify functional programs written using the state monad. It uses Coq’s Program framework to provide strong specifications for the standard operations that the state monad supports, such as return and bind. By exploiting the monadic structure of such programs during the verification process, it becomes easier to prove that they satisfy their specification.

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: Wouter Swierstra
• Keywords: Artificial Intelligence, Coq’s Program Framework, Functional Programs, State Monad, TPHOL 2009