The typed lambda-calculus is not elementary recursive
From MaRDI portal
Cites work
- A theory of prepositional types
- A unification algorithm for typed -calculus
- Completeness, invariance and λ-definability
- Definierbare Funktionen imλ-Kalkül mit Typen
- Fully abstract models of typed \(\lambda\)-calculi
- Godel's interpretation of intuitionism
- scientific article; zbMATH DE number 3485758 (Why is no real title available?)
- scientific article; zbMATH DE number 3561331 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3342819 (Why is no real title available?)
- scientific article; zbMATH DE number 3423994 (Why is no real title available?)
- scientific article; zbMATH DE number 3083488 (Why is no real title available?)
- Intuitionistic propositional logic is polynomial-space complete
- On the computational power of pushdown automata
- The Connection between Equivalence of Proofs and Cartesian Closed Categories
- The polynomial-time hierarchy
Cited in
(44)- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Word operation definable in the typed -calculus
- On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
- Finitely stratified polymorphism
- A simple proof of a theorem of Statman
- Intuitionistic propositional logic is polynomial-space complete
- Ramified recurrence and computational complexity. III: Higher type recurrence and elementary complexity
- Ordinals and ordinal functions representable in the simply typed lambda calculus
- Functions over free algebras definable in the simply typed lambda calculus
- Parallel beta reduction is not elementary recursive
- (Optimal) duplication is not elementary recursive
- A formal system of reduction paths for parallel reduction
- An abstract approach to stratification in linear logic
- Decidability of bounded higher-order unification
- Ensuring termination by typability
- The role of polymorphism in the characterisation of complexity by soft types
- Complexity hierarchies beyond elementary
- A logical framework with explicit conversions
- On session types and polynomial time
- On higher-order probabilistic subrecursion
- λ-definable functionals andβη conversion
- Least upper bounds on the size of Church-Rosser diagrams in term rewriting and -calculus
- Completeness, invariance and λ-definability
- Upper bounds for standardizations and an application
- Fully abstract translations between functional languages
- The Impact of the Lambda Calculus in Logic and Computer Science
- An analysis of the Core-ML language: Expressive power and type reconstruction
- The complexity of type inference for higher-order typed lambda calculi
- The complexity of higher-order queries
- On higher-order probabilistic subrecursion
- scientific article; zbMATH DE number 7561616 (Why is no real title available?)
- Many more predecessors: a representation workout
- Is the Optimal Implementation Inefficient? Elementarily Not
- Lambda-representable functions over term algebras
- Functional programs as compressed data
- A characterization of lambda-terms transforming numerals
- The most nonelementary theory
- Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
- Functional interpretations of feasibly constructive arithmetic
- Proof-theoretic investigation of -reduction in the simply typed -calculus
- The semantics of second-order lambda calculus
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- A characterization of lambda definable tree operations
- On the membership problem for non-linear abstract categorial grammars
This page was built for publication: The typed lambda-calculus is not elementary recursive
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1259590)
