Reasoning about effectful programs and evaluation order

Add to your list(s) Download to your calendar using vCal

• Dylan McDermott (Cambridge)
• Friday 31 May 2019, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Benedikt Ahrens.

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 .

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.