University of Birmingham > Talks@bham > Theoretical computer science seminar > Reasoning about effectful programs and evaluation order

Reasoning about effectful programs and evaluation order

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.