The duality of computation

Abstract : We present the lambda-bar-mu-mu-tilde-calculus, a syntax for lambda-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen's sequent calculus LK, a key classical logical system in proof theory. Under the Curry-Howard correspondence between proofs and programs, we can see LK, or more precisely a formulation called LK-mu-mu-tilde, as a syntax-directed system of simple types for lambda-bar-mu-mu-tilde-calculus. For lambda-bar-mu-mu-tilde-calculus, choosing a call-by-name or call-by-value discipline for reduction amounts to choosing one of the two possible symmetric orientations of a critical pair. Our analysis leads us to revisit the question of what is a natural syntax for call-by-value functional computation. We define a translation of lambda-mu-calculus into lambda-bar-mu-mu-tilde-calculus and two dual translations back to lambda-calculus, and we recover known CPS translations by composing these translations.
Type de document :
Communication dans un congrès
Fifth ACM SIGPLAN International Conference on Functional Programming : ICFP '00, Sep 2000, Montréal, Canada. ACM, 35/9 (9), pp.233-243, 2000, SIGPLAN Notice
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-00156377
Contributeur : Hugo Herbelin <>
Soumis le : mercredi 20 juin 2007 - 20:31:50
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : jeudi 8 avril 2010 - 20:57:00

Fichiers

icfp-CuHer00-duality_errata.pd...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00156377, version 1

Collections

INRIA | PPS | USPC

Citation

Hugo Herbelin, Pierre-Louis Curien. The duality of computation. Fifth ACM SIGPLAN International Conference on Functional Programming : ICFP '00, Sep 2000, Montréal, Canada. ACM, 35/9 (9), pp.233-243, 2000, SIGPLAN Notice. 〈inria-00156377〉

Partager

Métriques

Consultations de la notice

347

Téléchargements de fichiers

304