Termination of lambda-calculus with the extra Call-By-Value rule known as assoc.

Abstract : In this paper we prove that any lambda-term that is strongly normalising for beta-reduction is also strongly normalising for beta,assoc-reduction. assoc is a call-by-value rule that has been used in works by Moggi, Joachimsky, Espirito Santo and others. The result has often been justified with incomplete or incorrect proofs. Here we give one in full details.
Type de document :
Pré-publication, Document de travail
2007
Liste complète des métadonnées


https://hal.inria.fr/inria-00292029
Contributeur : Stéphane Graham-Lengrand <>
Soumis le : mardi 2 septembre 2008 - 18:35:47
Dernière modification le : jeudi 9 février 2017 - 15:12:24
Document(s) archivé(s) le : samedi 26 novembre 2016 - 01:11:54

Fichiers

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

Identifiants

  • HAL Id : inria-00292029, version 2
  • ARXIV : 0806.4859

Collections

Citation

Stéphane Lengrand. Termination of lambda-calculus with the extra Call-By-Value rule known as assoc.. 2007. <inria-00292029v2>

Partager

Métriques

Consultations de
la notice

168

Téléchargements du document

50