Substitution revisited

DOI10.1016/0304-3975(88)90149-1zbMath0651.03008OpenAlexW2913281688MaRDI QIDQ1106190

Allen Stoughton

Publication date: 1988

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(88)90149-1

zbMATH Keywords

denotational semanticscpostructural recursionalpha-congruencesimultaneous substitutionuntyped lambda- calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items

Formal metatheory of the lambda calculus using Stoughton's substitution, Secure mechanical verification of mutually recursive procedures, The Qu-Prolog unification algorithm: formalisation and correctness, A canonical locally named representation of binding, Timing and causality in process algebra, Rensets and renaming-based recursion for syntax with bindings extended version, Simultaneous substitution in the typed lambda calculus, A Formal Proof of the Strong Normalization Theorem for System T in Agda, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda, Strong categorical datatypes II: A term logic for categorical programming, A formalized general theory of syntax with bindings: extended version, Alpha-structural induction and recursion for the lambda calculus in constructive type theory, Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax, Mechanical verification of mutually recursive procedures, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, External and internal syntax of the \(\lambda \)-calculus, A conservative look at operational semantics with variable binding, The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective), Term-generic logic, Nominal Equational Logic

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Axioms for the Theory of Lambda-Conversion
• The Category-Theoretic Solution of Recursive Domain Equations
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Unnamed Item
• Unnamed Item