Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus

DOI10.1016/j.entcs.2015.04.013zbMath1342.68055OpenAlexW2051367997WikidataQ113317801 ScholiaQ113317801MaRDI QIDQ530864

Nora Szasz, Álvaro Tasistro, Ernesto Copello

Publication date: 1 August 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.04.013

zbMATH Keywords

constructive type theorylambda calculusformal metatheory

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Other constructive mathematics (03F65) Combinatory logic and lambda calculus (03B40)

Related Items

Formal metatheory of the lambda calculus using Stoughton's substitution, A Formal Proof of the Strong Normalization Theorem for System T in Agda, Alpha-structural induction and recursion for the lambda calculus in constructive type theory

Cites Work

• Viewing \({\lambda}\)-terms through maps
• Substitution revisited
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• Nominal unification
• Nominal logic, a first order theory of names and binding
• The locally nameless representation
• Some lambda calculus and type theory formalized
• Engineering formal metatheory
• Alpha-structural recursion and induction
• Axioms for the Theory of Lambda-Conversion
• The next 700 programming languages
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item