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

DOI10.1016/J.ENTCS.2015.04.013zbMATH Open1342.68055OpenAlexW2051367997WikidataQ113317801 ScholiaQ113317801MaRDI QIDQ530864FDOQ530864

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

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

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)

Cites Work

• Nominal logic, a first order theory of names and binding
• Some lambda calculus and type theory formalized
• Alpha-structural recursion and induction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Nominal unification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Engineering formal metatheory
• Title not available (Why is that?)
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• The next 700 programming languages
• Title not available (Why is that?)
• Substitution revisited
• The locally nameless representation
• Operational techniques in PVS -- a preliminary evaluation
• Nominal reasoning techniques in Coq (extended abstract)
• Axioms for the Theory of Lambda-Conversion
• Title not available (Why is that?)
• Viewing \({\lambda}\)-terms through maps

Cited In (8)

• Simultaneous substitution in the typed lambda calculus
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Substitution revisited
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Title not available (Why is that?)
• 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)