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

DOI10.1016/0020-0190(93)90198-IMaRDI QIDQ1802059zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

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

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

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

Cites work

• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A mechanical proof of the Church-Rosser theorem
• Categorical combinators
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(3)

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

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)