ICE-TCS seminar: Dylan McDermott
On the relation between call-by-value and call-by-name
ICE-TCS seminar #342
Date and time: Monday, 4 November 2019, 11:50-12:35
Location: Room M1.06
Speaker: Dylan McDermott (Reykjavik University)
Title: On the relation between call-by-value and call-by-name
Abstract: In languages with side-effects, the behaviour of programs depends on the evaluation order we use, but two different evaluation orders often have related behaviours. For example, if a program might diverge but otherwise has no side-effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name (but the converse is not true).
I will talk about a technique for relating call-by-value and call-by-name executions of programs. The key ingredient is Levy’s call-by-push-value calculus (CBPV), which provides a framework for reasoning about evaluation orders. The technique is to define maps between the call-by-value and call-by-name interpretations of types in CBPV, and then identify properties of side-effects that imply these maps form a Galois connection. This gives rise to a general reasoning principle that relates call-by-value and call-by-name for various side-effects.
