A proof of the substitution lemma in de Bruijn's notation

DOI10.1016/0020-0190(93)90198-IzbMATH Open0770.68088OpenAlexW2010072737WikidataQ124873174 ScholiaQ124873174MaRDI QIDQ1802059FDOQ1802059

Authors: Hiroshi Ohtsuka 

Publication date: 1993

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(93)90198-i

Recommendations

• Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems
• Proof Pearl: De Bruijn Terms Really Do Work
• de Bruijn notation as a nested datatype
• The soundness of explicit substitution with nameless variables
• A notation for lambda terms. A generalization of environments

zbMATH Keywords

\(\lambda\)-calculusde Bruijn's notationsubstitution lemma

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Title not available (Why is that?)
• Categorical combinators
• A mechanical proof of the Church-Rosser theorem

Cited In (3)

• On Levenshtein’s Reconstruction Problem Under Insertions, Deletions, and Substitutions
• Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
• Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems

This page was built for publication: A proof of the substitution lemma in de Bruijn's notation

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