Completeness, invariance and λ-definability

DOI10.2307/2273377MaRDI QIDQ3947643zbMATHOpenAlexFDO

Authors Richard Statman

Publication date 1982

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2307/2273377

zbMATH Keywords

lambda definabilitylambda conversionterm modelsmodels of typed lambda calculus

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Cites work

• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• Mechanizing \(\omega\)-order type theory through unification
• The typed lambda-calculus is not elementary recursive

Cited in

(26)

• The Typed Böhm Theorem
• Extended First-Order Logic
• Proofs as processes
• Dependency Tree Automata
• On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
• The simply typed theory of \(\beta\)-conversion has no maximum extension
• An alternate proof of Statman's finite completeness theorem
• Third order matching is decidable
• Proof of a conjecture of S. Mac Lane
• Kripke-style models for typed lambda calculus
• Recognizability in the Simply Typed Lambda-Calculus
• The IO and OI hierarchies revisited
• An intersection problem for finite automata
• Reflections on a Theorem of Henkin
• Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus
• Equality between functionals in the presence of coproducts
• A simple proof of a theorem of Statman
• Decidability of all minimal models
• Extensional models for polymorphism
• Linear realizability and full completeness for typed lambda-calculi
• λ-definable functionals andβη conversion
• The typed lambda-calculus is not elementary recursive
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• Polymorphic rewriting conserves algebraic strong normalization
• Weak typed Böhm theorem on IMLL
• On the \(\lambda Y\) calculus

This page was built for publication: Completeness, invariance and λ-definability

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