Completeness, invariance and λ-definability

DOI10.2307/2273377zbMATH Open0487.03006OpenAlexW1497630311MaRDI QIDQ3947643FDOQ3947643

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

• The typed lambda-calculus is not elementary recursive
• Title not available (Why is that?)
• Mechanizing \(\omega\)-order type theory through unification

Cited In (27)

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