Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)

DOI10.1007/3-540-61464-8_52zbMATH Open1503.03026OpenAlexW1559970946MaRDI QIDQ5055860FDOQ5055860

Authors: Delia Kesner 

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61464-8_52

Recommendations

• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Confluence properties of weak and strong calculi of explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• Eta-conversion for the languages of explicit substitutions

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Explicit substitutions with de bruijn's levels
• Explicit substitutions
• Title not available (Why is that?)
• Title not available (Why is that?)
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Explicit substitutions à la de Bruijn: the local and global way
• Title not available (Why is that?)
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• The virtues of eta-expansion
• Some lambda calculi with categorical sums and products
• Title not available (Why is that?)
• Proof of termination of the rewriting system SUBSET on CCL
• Confluence properties of weak and strong calculi of explicit substitutions
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Title not available (Why is that?)
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• Title not available (Why is that?)
• Eta-conversion for the languages of explicit substitutions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• Strong normalization of substitutions

Cited In (5)

• The Expansion Problem in Lambda Calculi with Explicit Substitution
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• Title not available (Why is that?)
• Erratum: Eta-conversion for the languages of explicit substitutions
• An Output-Based Semantics of Λμ with Explicit Substitution in the π-Calculus

This page was built for publication: Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)

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