A predicate transformer semantics for effects
Date: Wed, June 23, 2021
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.