Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
From MaRDI portal
Publication:6635503
DOI10.46298/LMCS-20(3:21)2024MaRDI QIDQ6635503
Publication date: 12 November 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Bridging Curry and Church's typing style
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- A simple proof of a theorem of Statman
- The typed lambda-calculus is not elementary recursive
- A trace semantics for System F parametric polymorphism
- Database query languages embedded in the typed lambda calculus
- An upper bound for reduction sequences in the typed \(\lambda\)-calculus
- Exact bounds for lengths of reductions in typed \(\lambda\)-calculus
- Complexity hierarchies beyond elementary
- The complexity of regular(-like) expressions
- Simply typed fixpoint calculus and collapsible pushdown automata
- A By-Level Analysis of Multiplicative Exponential Linear Logic
- Polarised Intermediate Representation of Lambda Calculus with Sums
- The Dot-Depth Hierarchy, 45 Years Later
- Term Rewriting and All That
- Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus
- The Cost of Usage in the ?-Calculus
- Deciding equivalence with sums and the empty type
- The Safe Lambda Calculus
- Parallel reductions in \(\lambda\)-calculus
- Higher-order quantified Boolean satisfiability
- Two decreasing measures for simply typed \(\lambda\)-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)
