Comparing calculi of explicit substitutions with eta-reduction

Mauricio Ayala-Rincón, F. L C De Moura, Fairouz Kamareddine

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous work has illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. Three styles of explicit substitutions are treated in this paper: the ?s and the ?se which have proved useful for solving practical problems like higher order unification, and the suspension calculus related to the implementation of the language ?-Prolog. We enlarge the suspension calculus with an adequate eta-reduction which we show to preserve termination and confluence of the associated substitution calculus and to correspond to the eta-reductions of the other two calculi. Additionally, we prove that ?s and ?se as well as ?s and the suspension calculus are non comparable while ?se is more adequate than the suspension calculus. ©2002 Published by Elsevier Science B.V.

Original languageEnglish
Pages (from-to)79-98
Number of pages20
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - Oct 2002
Event9th Workshop on Logic, Language, Information and Computation - Rio de Janeiro, Brazil
Duration: 30 Jul 20022 Aug 2002


  • Calculi of explicit substitutions
  • Eta reduction
  • Lambda-calculi


Dive into the research topics of 'Comparing calculi of explicit substitutions with eta-reduction'. Together they form a unique fingerprint.

Cite this