Control Reduction Theories: the Benefit of Structural Substitution

Zena Ariola 1 Hugo Herbelin 2
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : The historical design of the call-by-value theory of control relies on the reification of evaluation contexts as regular functions and on the use of ordinary term application for jumping to a continuation. To the contrary, the lambda-C-tp control calculus, developed by the authors, distinguishes between jumps and terms. This alternative calculus, which derives from Parigot's lambda-mu-calculus, works by direct "structural substitution" of evaluation contexts. We review and revisit the legacy theories of control and argue that lambda-C-tp provides an observationally equivalent but smoother theory. In an additional note contributed by Matthias Felleisen, we review the story of the birth of control calculi during the mid to late eighties at Indiana University.
Type de document :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 2007
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00177320
Contributeur : Hugo Herbelin <>
Soumis le : dimanche 7 octobre 2007 - 15:22:57
Dernière modification le : jeudi 10 mai 2018 - 01:09:56
Document(s) archivé(s) le : dimanche 11 avril 2010 - 22:21:33

Fichier

jfp-AriHer07-lambda-C-tp.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00177320, version 1

Collections

Citation

Zena Ariola, Hugo Herbelin. Control Reduction Theories: the Benefit of Structural Substitution. Journal of Functional Programming, Cambridge University Press (CUP), 2007. 〈inria-00177320〉

Partager

Métriques

Consultations de la notice

232

Téléchargements de fichiers

117