Continuation-and-environment-passing style translations: a focus on call-by-need - Université Sorbonne Paris Cité Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2019

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

Résumé

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.
Fichier principal
Vignette du fichier
esop19.pdf (612.46 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01972846 , version 1 (08-01-2019)

Identifiants

  • HAL Id : hal-01972846 , version 1

Citer

Hugo Herbelin, Étienne Miquey. Continuation-and-environment-passing style translations: a focus on call-by-need. 2019. ⟨hal-01972846⟩
150 Consultations
459 Téléchargements

Partager

Gmail Facebook X LinkedIn More