SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★

DOI10.3166/jancl.16.119-150zbMath1184.68469OpenAlexW1997707012WikidataQ58001512 ScholiaQ58001512MaRDI QIDQ3647258

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

Publication date: 30 November 2009

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3166/jancl.16.119-150

zbMATH Keywords

\(\lambda\)-calculusexplicit substitutionsvisualization of \(\beta\)- and \(\eta\)-contraction and normalization

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

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

Uses Software

• Automath

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Choices in representation and reduction strategies for lambda terms in intensional contexts
• A notation for lambda terms. A generalization of environments
• An analysis of Böhm's theorem
• A useful \(\lambda\)-notation
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Higher order unification via explicit substitutions
• Nominal unification
• Unification via the  se-style of explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Relating the   - and  s-styles of explicit substitutions
• The λs_e-calculus does not preserve strong normalisation
• Closed reduction: explicit substitutions without $\alpha$ -conversion
• Term Rewriting and All That
• Explicit substitutions