On explicit substitution with names

DOI10.1007/s10817-011-9222-5zbMath1269.68044OpenAlexW2085041284MaRDI QIDQ2392486

Roel Bloo, Kristoffer H. Rose, Frédéric Lang

Publication date: 1 August 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-011-9222-5

zbMATH Keywords

confluenceexplicit substitutionopen termspreservation of strong normalization

Mathematics Subject Classification ID

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

Uses Software

• Nominal Isabelle

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An abstract framework for environment machines
• Resource operators for \(\lambda\)-calculus
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• Nominal techniques in Isabelle/HOL
• Termination of rewriting
• Explicit substitution. On the edge of strong normalization
• Combinatory reduction systems: Introduction and survey
• Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
• Lambda-calculus with director strings
• Nominal rewriting
• A λ-calculus with explicit weakening and explicit substitution
• λν, a calculus of explicit substitutions which preserves strong normalisation
• A Theory of Explicit Substitutions with Safe and Full Composition
• A Rewriting System for Categorical Combinators with Multiple Arguments
• The Theory of Calculi with Explicit Substitutions Revisited
• Axioms for the Theory of Lambda-Conversion
• ON STEPWISE EXPLICIT SUBSTITUTION
• Confluence properties of weak and strong calculi of explicit substitutions
• On explicit substitutions and names (extended abstract)
• Term Rewriting and All That
• Proof nets and explicit substitutions
• Explicit substitutions
• Delayed Substitutions
• Tree-Manipulating Systems and Church-Rosser Theorems
• The Mechanical Evaluation of Expressions

This page was built for publication: On explicit substitution with names