Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
From MaRDI portal
Publication:1407578
DOI10.1007/s00153-002-0156-9zbMath1025.03010OpenAlexW1991947308MaRDI QIDQ1407578
Felix Joachimski, Ralph Matthes
Publication date: 16 September 2003
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00153-002-0156-9
Related Items (30)
A semantical proof of the strong normalization theorem for full propositional classical natural deduction ⋮ Syntactic analysis of \(\eta\)-expansions in pure type systems. ⋮ Elementary Proof of Strong Normalization for Atomic F ⋮ A Formal Proof of the Strong Normalization Theorem for System T in Agda ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Polarised subtyping for sized types ⋮ Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda ⋮ Proof Terms for Generalized Natural Deduction ⋮ A short proof of the strong normalization of classical natural deduction with disjunction ⋮ A domain model characterising strong normalisation ⋮ Atomic polymorphism ⋮ Strong normalization of classical natural deduction with disjunctions ⋮ Continuous normalization for the lambda-calculus and Gödel's T ⋮ Non-strictly positive fixed points for classical natural deduction ⋮ Introduction to Type Theory ⋮ Validity concepts in proof-theoretic semantics ⋮ Monotone (co)inductive types and positive fixed-point types ⋮ The \(\lambda \)-calculus and the unity of structural proof theory ⋮ Prawitz, Proofs, and Meaning ⋮ Cut Elimination, Substitution and Normalisation ⋮ Meaning in Use ⋮ Implementing a normalizer using sized heterogeneous types ⋮ An arithmetic for non-size-increasing polynomial-time computation ⋮ The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) ⋮ Higher type recursion, ramification and polynomial time ⋮ A simple proof of second-order strong normalization with permutative conversions ⋮ Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus ⋮ Normalization for the Simply-Typed Lambda-Calculus in Twelf ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention ⋮ CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI
This page was built for publication: Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
