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

DOI10.1016/J.ENTCS.2015.04.013MaRDI QIDQ530864zbMATH OpenOpenAlexWikidataFDO

Authors Álvaro Tasistro, Ernesto Copello, Nora Szasz

Publication date 1 August 2016

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

zbMATH Keywords

lambda calculusconstructive type theoryformal metatheory

Mathematics Subject Classification ID

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

Recommendations

• Formal metatheory of the lambda calculus using Stoughton's substitution
• Axioms for the Theory of Lambda-Conversion
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Some lambda calculus and type theory formalized
• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions

Cites work

• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3961577 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 612169 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• Alpha-structural recursion and induction
• Axioms for the Theory of Lambda-Conversion
• Engineering formal metatheory
• Nominal logic, a first order theory of names and binding
• Nominal reasoning techniques in Coq (extended abstract)
• Nominal unification
• Operational techniques in PVS -- a preliminary evaluation
• Some lambda calculus and type theory formalized
• Substitution revisited
• The locally nameless representation
• The next 700 programming languages
• Viewing \({\lambda}\)-terms through maps

Cited in

(8)

• Simultaneous substitution in the typed lambda calculus
• scientific article; zbMATH DE number 800564 (Why is no real title available?)
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Substitution revisited
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• A Formal Proof of the Strong Normalization Theorem for System T in Agda
• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions

This page was built for publication: Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus

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