An alternate proof of Statman's finite completeness theorem

DOI10.1016/J.IPL.2012.04.014MaRDI QIDQ436624zbMATH OpenOpenAlexFDO

Authors B. Srivathsan, Igor Walukiewicz

Publication date 25 July 2012

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2012.04.014

zbMATH Keywords

formal semanticssimply typed lambda calculustheory of computation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Statman's 1-section theorem
• Strong typed Böhm theorem and functional completeness on the linear lambda calculus
• Typed Lambda Calculi and Applications
• A simple proof of a theorem of Statman
• Order-incompleteness and finite lambda reduction models

Cites work

• Completeness in the theory of types
• Completeness, invariance and λ-definability
• scientific article; zbMATH DE number 1984520 (Why is no real title available?)
• On the membership problem for non-linear abstract categorial grammars
• Recognizability in the Simply Typed Lambda-Calculus
• The Clausal Theory of Types

Cited in

(4)

• Statman's 1-section theorem
• The IO and OI hierarchies revisited
• A brief proof of the full completeness of Shin's Venn diagram proof system
• Syntactically and semantically regular languages of -terms coincide through logical relations

This page was built for publication: An alternate proof of Statman's finite completeness theorem

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