A predicate transformer semantics for effects

Wouter Swierstra

Reasoning about programs that use effects can be much harder than reasoning about their pure counterparts. In this talk I will present a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction.

---

Previous: Aron Zwaan | Implicit Incremental Type Checking
Next: Marco Vassena | Towards Principled and Reliable Software System Security