A simple proof of a theorem of Statman

DOI10.1016/0304-3975(92)90020-GMaRDI QIDQ1199546zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 814613
• Statman's hierarchy theorem
• Statman's 1-section theorem
• scientific article; zbMATH DE number 2185660
• A decidable theory of type assignment

Cites work

• A theory of prepositional types
• Completeness, invariance and λ-definability
• scientific article; zbMATH DE number 3561331 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• The complexity of theorem-proving procedures
• The polynomial-time hierarchy
• The typed lambda-calculus is not elementary recursive

Cited in

(16)

• A simple proof of the majorizing measure theorem
• Parallel beta reduction is not elementary recursive
• (Optimal) duplication is not elementary recursive
• Statman's 1-section theorem
• Enumerators of lambda terms are reducing constructively
• On session types and polynomial time
• scientific article; zbMATH DE number 7227789 (Why is no real title available?)
• An alternate proof of Statman's finite completeness theorem
• Statman's hierarchy theorem
• 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
• scientific article; zbMATH DE number 7561616 (Why is no real title available?)
• The most nonelementary theory
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• Implicit automata in typed -calculi I: aperiodicity in a non-commutative logic

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1199546)