Comparing and implementing calculi of explicit substitutions with eta-reduction

DOI10.1016/J.APAL.2004.06.009zbMath1067.03042OpenAlexW2023051485WikidataQ58001518 ScholiaQ58001518MaRDI QIDQ1779307

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

Publication date: 1 June 2005

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2004.06.009

zbMATH Keywords

explicit substitutions\(\lambda\)-calculieta-reductionsuspension calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Related Items (3)

Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions ⋮ A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★

Uses Software

• Automath
• ALF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• 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
• Bridging de Bruijn indices and variable names in explicit substitutions calculi
• 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
• The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations
• Explicit Substitutions à la de Bruijn
• Explicit substitutions
• Explicit substitutions with de bruijn's levels
• Combinatory reduction systems with explicit substitution that preserve strong normalisation

This page was built for publication: Comparing and implementing calculi of explicit substitutions with eta-reduction