Pages that link to "Item:Q1407578"

The following pages link to Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\) (Q1407578):

Displaying 34 items.

• A short proof that adding some permutation rules to \(\beta \) preserves SN (Q631758) (← links)
• The \(\lambda \)-calculus and the unity of structural proof theory (Q733755) (← links)
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction (Q818927) (← links)
• A domain model characterising strong normalisation (Q958484) (← links)
• Higher type recursion, ramification and polynomial time (Q1577477) (← links)
• Continuous normalization for the lambda-calculus and Gödel's T (Q1772771) (← links)
• Non-strictly positive fixed points for classical natural deduction (Q1772778) (← links)
• An arithmetic for non-size-increasing polynomial-time computation (Q1827388) (← links)
• Syntactic analysis of \(\eta\)-expansions in pure type systems. (Q1873755) (← links)
• Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda (Q2229159) (← links)
• Strong normalization of classical natural deduction with disjunctions (Q2482841) (← links)
• Validity concepts in proof-theoretic semantics (Q2500820) (← links)
• A simple proof of second-order strong normalization with permutative conversions (Q2566069) (← links)
• (Q2778886) (← links)
• The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
• Normalization for the simply-typed lambda-calculus in Twelf (Q2871835) (← links)
• Elementary Proof of Strong Normalization for Atomic F (Q2957669) (← links)
• Polarised subtyping for sized types (Q3535676) (← links)
• Implementing a normalizer using sized heterogeneous types (Q3638918) (← links)
• (Q4323124) (← links)
• A short proof of the strong normalization of classical natural deduction with disjunction (Q4650284) (← links)
• Atomic polymorphism (Q4916559) (← links)
• Monotone (co)inductive types and positive fixed-point types (Q4943545) (← links)
• Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention (Q5022932) (← links)
• CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI (Q5024505) (← links)
• POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
• Introduction to Type Theory (Q5191087) (← links)
• Prawitz, Proofs, and Meaning (Q5213604) (← links)
• Cut Elimination, Substitution and Normalisation (Q5213610) (← links)
• Meaning in Use (Q5213613) (← links)
• Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus (Q5251184) (← links)
• Proof Terms for Generalized Natural Deduction (Q6060674) (← links)
• A Formal Proof of the Strong Normalization Theorem for System T in Agda (Q6118750) (← links)
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications (Q6597960) (← links)