On explicit substitution with names

DOI10.1007/S10817-011-9222-5zbMATH Open1269.68044OpenAlexW2085041284MaRDI QIDQ2392486FDOQ2392486

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

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

zbMATH Keywords

confluenceexplicit substitutionopen termspreservation of strong normalization

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

• On explicit substitutions and names (extended abstract)
• On the rule of \(k\) names

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)