Normalization and continuation-passing-style interpretation of simply-typed call-by-need λ-calculus with control

Hugo Herbelin 1, 2 Étienne Miquey 1, 2, 3
1 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : Ariola et al defined a call-by-need λ-calculus with control, together with a sequent calculus presentation of it. They mechanically derive from the sequent calculus presentation a continuation-passing-style transformation simulating the reduction. In this paper, we consider the simply-typed version of the calculus and prove its normalization by means of a realizability interpretation. This justifies a posteriori the design choice of the translation, and is to be contrasted with Okasaki et al. semantics which is not normalizing even in the simply-typed case. Besides, we also present a type system for the target language of the continuation-passing-style translation. Furthermore, the call-by-need calculus we present makes use of an explicit environment to lazily store and share computations. We rephrase the calculus (as well as the translation) to use De Bruijn levels as pointers to this shared environment. This has the twofold benefit of solving a problem of α-conversion in Ariola et al calculus and of unveiling an interesting bit of computational content (within the continuation-passing-style translation) related to environment extensions.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01570987
Contributeur : Étienne Miquey <>
Soumis le : mardi 1 août 2017 - 13:09:37
Dernière modification le : jeudi 11 janvier 2018 - 06:28:03

Fichier

cbncps.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01570987, version 1

Collections

Citation

Hugo Herbelin, Étienne Miquey. Normalization and continuation-passing-style interpretation of simply-typed call-by-need λ-calculus with control. 2017. 〈hal-01570987〉

Partager

Métriques

Consultations de la notice

107

Téléchargements de fichiers

16