Termination of lambda-calculus with the extra Call-By-Value rule known as assoc. - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2007

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

Résumé

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.
Fichier principal
Vignette du fichier
SigmaBeta.pdf (143.82 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00292029 , version 1 (30-06-2008)
inria-00292029 , version 2 (02-09-2008)

Identifiants

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

Citer

Stéphane Lengrand. Termination of lambda-calculus with the extra Call-By-Value rule known as assoc.. 2007. ⟨inria-00292029v2⟩
105 Consultations
76 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More