Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda

DOI10.1016/J.ENTCS.2020.08.010MaRDI QIDQ2229159zbMATH OpenOpenAlexWikidataFDO

Authors Sebastián Urciuoli, Álvaro Tasistro, Nora Szasz

Publication date 22 February 2021

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

zbMATH Keywords

constructive type theoryformal metatheorylambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Recommendations

• A formalization of strong normalization for simply-typed lambda-calculus and System F
• scientific article; zbMATH DE number 512769
• Formal metatheory of the lambda calculus using Stoughton's substitution
• Short Proofs of Strong Normalization
• Strong normalization in type systems: A model theoretical approach

Cites work

• Alpha-structural induction and recursion for the lambda calculus in constructive type theory
• Automated Deduction – CADE-20
• Formal metatheory of the lambda calculus using Stoughton's substitution
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory
• POPLMark reloaded: mechanizing proofs by logical relations
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Substitution revisited

Cited in

(6)

• A formalized proof of strong normalization for guarded recursive types
• A formalization of strong normalization for simply-typed lambda-calculus and System F
• scientific article; zbMATH DE number 512769 (Why is no real title available?)
• Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• A Formal Proof of the Strong Normalization Theorem for System T in Agda

Describes a project that uses

Uses Software

• PoplMark
• Nominal Isabelle

This page was built for publication: Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda

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