The typed λ-calculus is not elementary recursive
- 31 July 1979
- journal article
- Published by Elsevier in Theoretical Computer Science
- Vol. 9 (1) , 73-81
- https://doi.org/10.1016/0304-3975(79)90007-0
Abstract
No abstract availableKeywords
This publication has 7 references indexed in Scilit:
- Completeness, invariance and λ-definabilityThe Journal of Symbolic Logic, 1982
- Intuitionistic propositional logic is polynomial-space completeTheoretical Computer Science, 1979
- Fully abstract models of typed λ-calculiTheoretical Computer Science, 1977
- The polynomial-time hierarchyTheoretical Computer Science, 1976
- The Connection between Equivalence of Proofs and Cartesian Closed CategoriesProceedings of the London Mathematical Society, 1975
- A unification algorithm for typed
- A theory of prepositional typesFundamenta Mathematicae, 1963