On explicit substitution with names

DOI10.1007/S10817-011-9222-5MaRDI QIDQ2392486zbMATH OpenOpenAlexFDO

Authors Kristoffer H. Rose, Roel Bloo, 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

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

Recommendations

• On explicit substitutions and names (extended abstract)
• Explicit substitutions
• The soundness of explicit substitution with nameless variables
• scientific article; zbMATH DE number 1222417
• Term Rewriting and Applications
• ON STEPWISE EXPLICIT SUBSTITUTION
• scientific article; zbMATH DE number 1508928
• On the Notion of Substitution

Cites work

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

Cited in

(3)

• The soundness of explicit substitution with nameless variables
• On the rule of \(k\) names
• On explicit substitutions and names (extended abstract)

Describes a project that uses

Uses Software

• Nominal Isabelle

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

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