An Operational Account of Call-By-Value Minimal and Classical $\lambda$-calculus in ''Natural Deduction'' Form

Hugo Herbelin 1, 2 Stéphane Zimmermann 2
1 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 give a decomposition of the equational theory of call-by-value lambda-calculus into a confluent rewrite system made of three independent subsystems that refines Moggi's computational calculus: - the purely operational system essentially contains Plotkin's beta-v rule and is necessary and sufficient for the evaluation of closed terms; - the structural system contains commutation rules that are necessary and sufficient for the reduction of all ''computational'' redexes of a term, in a sense that we define; - the observational system contains rules that have no proper computational content but are necessary to characterize the valid observational equations on finite normal forms. We extend this analysis to the case of lambda-calculus with control and provide with the first presentation as a confluent rewrite system of Sabry-Felleisen and Hofmann's equational theory of lambda-calculus with control. Incidentally, we give an alternative definition of standardization in call-by-value lambda-calculus that, unlike Plotkin's original definition, prolongs weak head reduction in an unambiguous way.
Type de document :
Communication dans un congrès
Pierre-Louis Curien. TLCA 2009 - 9th International Conference on Typed Lambda-Calculi and Applications, Jul 2009, Brasilia, Brazil. Springer-Verlag, 5608, pp.142-156, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02273-9_12〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00389903
Contributeur : Hugo Herbelin <>
Soumis le : samedi 30 mai 2009 - 01:19:40
Dernière modification le : jeudi 15 novembre 2018 - 20:27:28
Document(s) archivé(s) le : lundi 15 octobre 2012 - 11:27:17

Fichier

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

Identifiants

Collections

Citation

Hugo Herbelin, Stéphane Zimmermann. An Operational Account of Call-By-Value Minimal and Classical $\lambda$-calculus in ''Natural Deduction'' Form. Pierre-Louis Curien. TLCA 2009 - 9th International Conference on Typed Lambda-Calculi and Applications, Jul 2009, Brasilia, Brazil. Springer-Verlag, 5608, pp.142-156, 2009, Lecture Notes in Computer Science. 〈10.1007/978-3-642-02273-9_12〉. 〈inria-00389903〉

Partager

Métriques

Consultations de la notice

354

Téléchargements de fichiers

195