A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
From MaRDI portal
Publication:4094853
DOI10.1112/jlms/s2-12.3.361zbMath0329.02010OpenAlexW2036605992MaRDI QIDQ4094853
Publication date: 1976
Published in: Journal of the London Mathematical Society (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1112/jlms/s2-12.3.361
Related Items
Infinitary lambda calculus and discrimination of Berarducci trees. ⋮ Relational graph models, Taylor expansion and extensionality ⋮ Easiness in graph models ⋮ Order-incompleteness and finite lambda reduction models ⋮ A characterization of F-complete type assignments ⋮ A General Class of Models of $\mathcal{H}^*$ ⋮ Type theories, normal forms, and \(D_{\infty}\)-lambda-models ⋮ Polymorphic type inference and containment ⋮ Full abstraction and recursion ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ \(\mathbb{T}^\omega\) as a universal domain ⋮ A syntactical proof of the operational equivalence of two \(\lambda\)-terms ⋮ Invertible terms in the lambda calculus ⋮ Algebraic interpretation of lambda calculus with resources ⋮ Parametric \(\lambda \)-theories ⋮ Böhm’s Theorem for Resource Lambda Calculus through Taylor Expansion ⋮ Some reasons for generalising domain theory ⋮ An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus ⋮ From Böhm's Theorem to Observational Equivalences ⋮ Strong normalization from an unusual point of view ⋮ An algebraic interpretation of the \(\lambda\beta K\)-calculus; and an application of a labelled \(\lambda\)-calculus ⋮ Aλδ-calculus with an algorithmicδ ⋮ Intersection types for \(\lambda\)-trees ⋮ Innocent game models of untyped \(\lambda\)-calculus ⋮ On the construction of stable models of untyped \(\lambda\)-calculus ⋮ Call-by-value Solvability ⋮ Lazy Lambda calculus: Theories, models and local structure characterization ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the semantics of the call-by-name CPS transform ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Unnamed Item ⋮ Completeness of type assignment in continuous lambda models ⋮ Definability and Full Abstraction ⋮ On infinite \(\eta\)-expansion ⋮ Classical lambda calculus in modern dress
