Abstract conditions for the confluence of explicit substitution calculi

Amelia Taylor

Research output: Contribution to journalArticlepeer-review


The aim of this paper is to give abstract properties of some calculi with explicit substitution which will be sufficient to prove their confluence. We define a property that we call "implementing a good notion of substitution." We show that calculi with explicit substitution having this property are confluent and their substitution reductions are also confluent. We test our theory with the well-known calculi of explicit substitution ?s, ?? and ?se. The latter is ?s with open terms. The property of implementing a good substitution is natural and characterizes a large number of calculi. Two conditions of this property are usually checked as an initial step in the proof for confluence. The third condition is new and is the key for our proofs of confluence. © 2005 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)213-228
Number of pages16
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 1 Mar 2005
Event2004 5th Asian Control Conference - Melbourne, Australia
Duration: 20 Jul 200423 Jul 2004


  • β-reduction
  • Confluence
  • Explicit substitution
  • Good substitution
  • Lambda calculi


Dive into the research topics of 'Abstract conditions for the confluence of explicit substitution calculi'. Together they form a unique fingerprint.

Cite this