A simple proof of a theorem of Statman

DOI10.1016/0304-3975(92)90020-GzbMath0762.03007OpenAlexW2016065322MaRDI QIDQ1199546

Harry G. Mairson

Publication date: 16 January 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(92)90020-g

zbMATH Keywords

\(\beta\eta\)-equality of first-order typeable \(\lambda\)-terms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (8)

(Optimal) duplication is not elementary recursive ⋮ The most nonelementary theory ⋮ On session types and polynomial time ⋮ An analysis of the Core-ML language: Expressive power and type reconstruction ⋮ The complexity of higher-order queries ⋮ Unnamed Item ⋮ Parallel beta reduction is not elementary recursive ⋮ The complexity of type inference for higher-order typed lambda calculi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The polynomial-time hierarchy
• The typed lambda-calculus is not elementary recursive
• Completeness, invariance and λ-definability
• A theory of prepositional types
• The complexity of theorem-proving procedures

This page was built for publication: A simple proof of a theorem of Statman