Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
From MaRDI portal
Publication:6635503
Recommendations
Cites work
- A By-Level Analysis of Multiplicative Exponential Linear Logic
- A simple proof of a theorem of Statman
- A trace semantics for System F parametric polymorphism
- An upper bound for reduction sequences in the typed -calculus
- Automatic synthesis of typed -programs on term algebras
- Bridging Curry and Church's typing style
- Complexity hierarchies beyond elementary
- Database query languages embedded in the typed lambda calculus
- Deciding equivalence with sums and the empty type
- Exact bounds for lengths of reductions in typed -calculus
- Higher-order quantified Boolean satisfiability
- Homogeneity without loss of generality
- scientific article; zbMATH DE number 4051569 (Why is no real title available?)
- scientific article; zbMATH DE number 512792 (Why is no real title available?)
- scientific article; zbMATH DE number 7029315 (Why is no real title available?)
- scientific article; zbMATH DE number 2087432 (Why is no real title available?)
- Parallel reductions in \(\lambda\)-calculus
- Polarised intermediate representation of lambda calculus with sums
- Semantic evaluation; intersection types and complexity of simply typed lambda calculus
- Simply typed fixpoint calculus and collapsible pushdown automata
- Term Rewriting and All That
- The complexity of regular(-like) expressions
- The cost of usage in the \(\lambda\)-calculus
- The dot-depth hierarchy, 45 years later
- The Safe Lambda Calculus
- The typed lambda-calculus is not elementary recursive
- Two decreasing measures for simply typed -terms
This page was built for publication: Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6635503)
