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

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

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 11 janvier 2018 - 06:19:44
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 de fichiers

53