Verifying higher-order programs with the dijkstra monad
Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, Benjamin Livshits · 2013
Modern programming languages, ranging from Haskell and ML, to JavaScript, C# and Java, all make extensive use of higher-order state. This paper advocates a new verification methodology for higher-order stateful programs, based on a new monad of predicate transformers called the Dijkstra monad.