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

DOI10.1007/3-540-61464-8_52MaRDI QIDQ5055860zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 2185655 (Why is no real title available?)
• scientific article; zbMATH DE number 2185658 (Why is no real title available?)
• scientific article; zbMATH DE number 2185670 (Why is no real title available?)
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• scientific article; zbMATH DE number 3573844 (Why is no real title available?)
• scientific article; zbMATH DE number 3609632 (Why is no real title available?)
• scientific article; zbMATH DE number 1300968 (Why is no real title available?)
• scientific article; zbMATH DE number 512797 (Why is no real title available?)
• scientific article; zbMATH DE number 1499112 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A confluent reduction for the extensional typed \(\lambda\)-calculus with pairs, sums, recursion and terminal object
• Combining algebraic rewriting, extensional lambda calculi, and fixpoints
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract)
• Confluence properties of weak and strong calculi of explicit substitutions
• Eta-conversion for the languages of explicit substitutions
• Explicit substitutions
• Explicit substitutions with de bruijn's levels
• Explicit substitutions à la de Bruijn: the local and global way
• Proof of termination of the rewriting system SUBSET on CCL
• Some lambda calculi with categorical sums and products
• Strong normalization of substitutions
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The virtues of eta-expansion
• λν, a calculus of explicit substitutions which preserves strong normalisation

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)
• scientific article; zbMATH DE number 6707782 (Why is no real title available?)
• 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)