HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Continuation-and-environment-passing style translations: a focus on call-by-need

Hugo Herbelin 1 Étienne Miquey 2
1 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, UPD7 - Université Paris Diderot - Paris 7
2 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
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, easing in particular the definition of continuation-passing style translations, the case of machines with global environments turns out to be much more subtle. The main purpose of this paper is to understand how to type a continuation-and-environment-passing style translations, that it to say how to soundly translate a classical calculus with environment into a calculus that does not have these features. To this end, we focus on a sequent calculus presentation of a call-by-need $λ$-calculus with classical control for which Ariola et. al already defined an untyped translation [5] and which we equipped with a system of simple types in a previous paper [32]. We present here a type system for the target language of their translation, which highlights a variant of Kripke forcing related to the environment-passing part of the translation. Finally, we show that our construction naturally handles the cases of call-by-name and call-by-value calculi with environment, encompassing in particular the Milner Abstract Machine, a machine with global environments for the call-by-name $λ$-calculus.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [49 references]  Display  Hide  Download

Contributor : Étienne Miquey Connect in order to contact the contributor
Submitted on : Tuesday, January 8, 2019 - 12:15:08 AM
Last modification on : Wednesday, April 27, 2022 - 3:47:59 AM
Long-term archiving on: : Tuesday, April 9, 2019 - 12:48:34 PM


Files produced by the author(s)


  • HAL Id : hal-01972846, version 1


Hugo Herbelin, Étienne Miquey. Continuation-and-environment-passing style translations: a focus on call-by-need. 2019. ⟨hal-01972846⟩



Record views


Files downloads