Classical Call-by-need and duality

Zena Ariola 1 Hugo Herbelin 2, 3 Alexis Saurin 2, 3
3 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We study call-by-need from the point of view of the duality between call-by-name and call-by-value. We develop sequent-calculus style versions of call-by-need both in the minimal and classical case. As a result, we obtain a natural extension of call-by-need with control operators. This leads us to introduce a call-by-need lambda-mu-calculus. Finally, by using the dualities principles of lambda-bar-mu-mu-tilde-calculus, we show the existence of a new call-by-need calculus, which is distinct from call-by-name, call-by-value and usual call-by-need theories.
Type de document :
Communication dans un congrès
C.-H. Luke Ong. TLCA 2011 - Typed Lambda Calculi and Applications, Jun 2011, Novi Sad, Serbia. Springer, 6690, pp.27-44, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21691-6_6〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00630156
Contributeur : Hugo Herbelin <>
Soumis le : vendredi 7 octobre 2011 - 14:42:03
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 13 novembre 2012 - 15:26:21

Fichier

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

Identifiants

Collections

INRIA | PPS | USPC

Citation

Zena Ariola, Hugo Herbelin, Alexis Saurin. Classical Call-by-need and duality. C.-H. Luke Ong. TLCA 2011 - Typed Lambda Calculi and Applications, Jun 2011, Novi Sad, Serbia. Springer, 6690, pp.27-44, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21691-6_6〉. 〈inria-00630156〉

Partager

Métriques

Consultations de la notice

183

Téléchargements de fichiers

112