![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Reasoning about effectful programs and evaluation order
Reasoning about effectful programs and evaluation orderAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsBritGrav 15 Electromagnetic Communications and Sensing Research Seminar Series EPS - College Research TeasOther talksCounting cycles in planar graphs TBA Quantum Sensing in Space TBA TBA TBC |