![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Environments & CPS translations, a well-typed story
Environments & CPS translations, a well-typed storyAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsData Science and Computational Statistics Seminar analysis PIPS - Postgraduate Informal Physics SeminarsOther talksDisorder relevance for non-convex random gradient Gibbs measures in d=2 Geometry of alternating projections in metric spaces with bounded curvature Modelling uncertainty in image analysis. TBC Metamaterials for light-matter interaction studies Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems |