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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292029
Contributor : Stéphane Graham-Lengrand <>
Submitted on : Tuesday, September 2, 2008 - 6:35:47 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:26 PM
Long-term archiving on : Saturday, November 26, 2016 - 1:11:54 AM

Files

SigmaBeta.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

205

Files downloads

117