![]() |
![]() |
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 listscomputer sience Featured lists Pure DétoursOther talksUltrafast Spectroscopy and Microscopy as probes of Energy Materials Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy TBA Life : it’s out there, but what and why ? Wave turbulence in the Schrödinger-Helmholtz equation TBA |