λ-definable functionals andβη conversion
From MaRDI portal
Publication:3322071
DOI10.1007/BF02023009zbMath0537.03009OpenAlexW2319619459MaRDI QIDQ3322071
Publication date: 1983
Published in: Archiv für Mathematische Logik und Grundlagenforschung (Search for Journal in Brave)
Full work available at URL: https://eudml.org/doc/138003
semanticscongruence relationtyped lambda calculustype structuresbeta-eta-conversionlambda definable functionalslambda-free functional equations
Related Items
Word operation definable in the typed \(\lambda\)-calculus ⋮ Weak typed Böhm theorem on IMLL ⋮ Provable isomorphisms of types ⋮ Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus ⋮ The relational model is injective for multiplicative exponential linear logic (without weakenings) ⋮ Unnamed Item ⋮ A characterization of lambda definable tree operations ⋮ Identity of Proofs Based on Normalization and Generality ⋮ The Typed Böhm Theorem ⋮ Linear realizability and full completeness for typed lambda-calculi ⋮ What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics ⋮ Extensional models for polymorphism ⋮ ETA-RULES IN MARTIN-LÖF TYPE THEORY ⋮ Prelogical relations
Cites Work