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, ...
Complete list of metadatas

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01972846
Contributor : Étienne Miquey <>
Submitted on : Tuesday, January 8, 2019 - 12:15:08 AM
Last modification on : Thursday, April 4, 2019 - 1:28:30 AM
Long-term archiving on : Tuesday, April 9, 2019 - 12:48:34 PM

File

esop19.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01972846, version 1

Citation

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

Share

Metrics

Record views

168

Files downloads

98