Reasoning about effectful programs and evaluation order

Given some program, we might ask whether replacing one evaluation order with another preserves the semantics. This is not the case in general for languages with side-effects, but can be for particular evaluation orders and particular side-effects. I will talk about how to prove equivalences between evaluation orders in the presence of some restriction on the side-effects of the language. I will focus on the example of call-by-value and call-by-name. The method uses call-by-push-value as an intermediate language that captures various evaluation orders. I will then talk about how to extend call-by-push-value to additionally support call-by-need, and how to prove an equivalence between call-by-need and call-by-name.

Part of this talk is based on the following paper: Dylan McDermott and Alan Mycroft. Extended call-by-push-value: reasoning about effectful programs and evaluation order. ESOP 2019.