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, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes
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, ...
Liste complète des métadonnées
Contributor : Étienne Miquey <>
Submitted on : Tuesday, January 8, 2019 - 12:15:08 AM
Last modification on : Thursday, April 4, 2019 - 1:28:30 AM
Document(s) archivé(s) le : 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