Completeness, invariance and λ-definability
From MaRDI portal
Publication:3947643
DOI10.2307/2273377zbMath0487.03006OpenAlexW1497630311MaRDI QIDQ3947643
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
Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)
Related Items (27)
Third order matching is decidable ⋮ On the \(\lambda Y\) calculus ⋮ Proofs as processes ⋮ Reflections on a Theorem of Henkin ⋮ Extended First-Order Logic ⋮ Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus ⋮ Weak typed Böhm theorem on IMLL ⋮ An intersection problem for finite automata ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Proof of a conjecture of S. Mac Lane ⋮ The simply typed theory of \(\beta\)-conversion has no maximum extension ⋮ Typing Weak MSOL Properties ⋮ An alternate proof of Statman's finite completeness theorem ⋮ On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems ⋮ Polymorphic rewriting conserves algebraic strong normalization ⋮ Decidability of all minimal models ⋮ A simple proof of a theorem of Statman ⋮ λ-definable functionals andβη conversion ⋮ The Typed Böhm Theorem ⋮ Linear realizability and full completeness for typed lambda-calculi ⋮ Dependency Tree Automata ⋮ The typed lambda-calculus is not elementary recursive ⋮ Extensional models for polymorphism ⋮ Recognizability in the Simply Typed Lambda-Calculus ⋮ Equality between functionals in the presence of coproducts ⋮ Kripke-style models for typed lambda calculus ⋮ The IO and OI hierarchies revisited
Cites Work
This page was built for publication: Completeness, invariance and λ-definability
