SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi

DOI10.3166/JANCL.16.119-150MaRDI QIDQ3647258zbMATH OpenOpenAlexWikidataFDO

Authors Flávio L. C. de Moura, Mauricio Ayala-Rincón, 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)

Recommendations

• A flexible framework for visualisation of computational properties of general explicit substitutions calculi
• Comparing calculi of explicit substitutions with eta-reduction
• Explicit substitutions
• A Theory of Explicit Substitutions with Safe and Full Composition
• The Theory of Calculi with Explicit Substitutions Revisited

Cites work

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

Cited in

(4)

• SUBSEXPL
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
• The Theory of Calculi with Explicit Substitutions Revisited
• A flexible framework for visualisation of computational properties of general explicit substitutions calculi

Describes a project that uses

Uses Software

• Automath

This page was built for publication: SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3647258)