Reasoning about effectful programs and evaluation order
- 14:00 5th June 2019 ( Trinity Term 2019 )Lecture Theatre B
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.