Sciweavers

TPHOL
2009
IEEE

A Hoare Logic for the State Monad

13 years 10 months ago
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.
Wouter Swierstra
Added 24 May 2010
Updated 24 May 2010
Type Conference
Year 2009
Where TPHOL
Authors Wouter Swierstra
Comments (0)