Comparing Calculi of Explicit Substitutions with Eta-reduction

DOI10.1016/S1571-0661(04)80542-5zbMath1261.03071OpenAlexW2158532214WikidataQ58001559 ScholiaQ58001559MaRDI QIDQ4916203

Mauricio Ayala-Rincón, Fairouz Kamareddine, Flávio L. C. de Moura

Publication date: 19 April 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)80542-5

zbMATH Keywords

lambda-calculicalculi of explicit substitutionseta reduction

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Uses Software

• Automath
• ALF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A notation for lambda terms. A generalization of environments
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A useful \(\lambda\)-notation
• Higher order unification via explicit substitutions
• Cut rules and explicit substitutions
• Unification via the  se-style of explicit substitutions
• λ-calculi with explicit substitutions and composition which preserve β-strong normalization
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Functional runtime systems within the lambda-sigma calculus
• ON STEPWISE EXPLICIT SUBSTITUTION
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Confluence properties of weak and strong calculi of explicit substitutions
• Relating the   - and  s-styles of explicit substitutions
• The λs_e-calculus does not preserve strong normalisation
• Explicit substitutions

This page was built for publication: Comparing Calculi of Explicit Substitutions with Eta-reduction