A predicate transformer semantics for effects

Wouter Swierstra

Date: Wed, June 23, 2021
Time: 12:00
Room: Eelco's Zoom Room

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 |
Next: Marco Vassena |