Relating the λσ- and λs-styles of explicit substitutions

Fairouz Kamareddine, Alejandro Rìos

Research output: Contribution to journalArticlepeer-review

16 Citations (Scopus)


Two methods of explicit substitutions, ?s- and ?s-styles, are compared. A criterion of adequacy is used to simulate ß-reduction in calculi of explicit substitutions and apply it to several calculi: ?s; ?s?; ?v; ?s; ?t; and ?u. Results proved that ?t is more adequate than ?v and that ?u is more adequate that ?v, ?s?, and ?s. Counterexamples is given to show that all other comparisons are impossible according to the criterion.

Original languageEnglish
Pages (from-to)349-380
Number of pages32
JournalJournal of Logic and Computation
Issue number3
Publication statusPublished - Jun 2000


Dive into the research topics of 'Relating the λσ- and λs-styles of explicit substitutions'. Together they form a unique fingerprint.

Cite this