Environments & CPS translations, a well-typed story

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

• Etienne Miquey, ENS Lyon
• Friday 19 March 2021, 14:00-15:00
• https://bham-ac-uk.zoom.us/j/81751920321?pwd=Vkk4NEtqNWl1TjhSeC9IN281KytnQT09.

If you have a question about this talk, please contact Vincent Rahli.

The call-by-need evaluation strategy for the λ-calculus is an evaluation strategy that lazily evaluates arguments only if needed, and if so, shares computations across all places where it is needed. To implement this evaluation strategy, abstract machines require some form of global environment. While abstract machines usually lead to a better understanding of the flow of control during the execution, facilitating in particular the definition of continuation-passing style translations, the case of machines with global environments turns out to be much more subtle. During this talk, we shall see how to soundly mix control operators and environments, by first proving the normalization of such a calculus using realizability techniques. The structure of the realizability interpretation will then help us to understand how to type a continuation-and-environment-passing style translation, that is to say how to soundly translate in continuation-passing style a calculus with global environment. We shall then present Fϒ, a generic calculus to define the target of such (typed) translations. In particular, Fϒ features a data type for typed stores and a mechanism of explicit coercions witnessing store extensions along environment-passing style translations. On the logical side, this broadly amounts to a Kripke forcing-like translation (for the environment-passing part) mixed with a negative translation (for the continuation-passing part). Since Fϒ allows for the definition of such translations for different source calculi (call-by-need, call-by-name, call-by-value) with different type systems (simple types, system F), we claim that it precisely captures the computational content of continuation-and-environment-passing style translations.

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
• Theoretical computer science seminar
• computer sience
• https://bham-ac-uk.zoom.us/j/81751920321?pwd=Vkk4NEtqNWl1TjhSeC9IN281KytnQT09

Note that ex-directory lists are not shown.