University of Birmingham > Talks@bham > Theoretical computer science seminar > Environments & CPS translations, a well-typed story

Environments & CPS translations, a well-typed story

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

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.

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 talks.cam from the University of Cambridge.