Pages that link to "Item:Q2758058"

The following pages link to Exact bounds for lengths of reductions in typed \(\lambda\)-calculus (Q2758058):

Displaying 22 items.

• A decidable theory of type assignment (Q365669) (← links)
• On the computational complexity of cut-reduction (Q636310) (← links)
• Reducibility of types in typed lambda calculus. Comment on a paper by Richard Statman (Q1104311) (← links)
• The Church-Rosser theorem and quantitative analysis of witnesses (Q1627965) (← links)
• Continuous normalization for the lambda-calculus and Gödel's T (Q1772771) (← links)
• Herbrand's theorem as higher order recursion (Q1987218) (← links)
• A formal system of reduction paths for parallel reduction (Q1989338) (← links)
• Exact bounds for acyclic higher-order recursion schemes (Q2112794) (← links)
• Decidability of bounded higher-order unification (Q2456577) (← links)
• Extracting Herbrand disjunctions by functional interpretation (Q2486989) (← links)
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus (Q2639840) (← links)
• Complexity hierarchies beyond elementary (Q2828216) (← links)
• Elementary Proof of Strong Normalization for Atomic F (Q2957669) (← links)
• Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence (Q2988360) (← links)
• A By-Level Analysis of Multiplicative Exponential Linear Logic (Q3182938) (← links)
• (Q4625705) (← links)
• Reducibility Proofs in the λ-Calculus (Q4903716) (← links)
• GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION (Q4977225) (← links)
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type (Q5111301) (← links)
• Typed Lambda Calculi and Applications (Q5704015) (← links)
• A quantitative model for simply typed λ-calculus (Q5875894) (← links)
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms (Q6635503) (← links)