Étienne Miquey

Abstract

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 (which one can think of as compilation processes), 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 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.