Set-theoretical and other elementary models of the \(\lambda\)-calculus

DOI10.1016/0304-3975(93)90094-AzbMath0790.03014MaRDI QIDQ1314361

Gordon D. Plotkin

Publication date: 22 June 1994

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

model theorylambda calculuscombinatory logicaxiom of foundationcomplete partial ordersset-theoretical model\(\lambda\beta\eta\)-calculusanti-foundation axiomsfilter modelsScott-Engeler algebras

Mathematics Subject Classification ID

Models of other mathematical theories (03C65) Combinatory logic and lambda calculus (03B40)

Related Items

Easy lambda-terms are not always simple ⋮ Easiness in graph models ⋮ Intersection types and lambda models ⋮ A decidable canonical representation of the compact elements in Scott's reflexive domain in \(P\omega\) ⋮ Enlargements of functional algebras for the lambda calculus ⋮ Graph lambda theories ⋮ Intuitionistic fixed point logic ⋮ Intersection types and domain operators ⋮ Behavioural inverse limit \(\lambda\)-models ⋮ Comparing models of the intensional typed \(\lambda\)-calculus ⋮ Uniqueness of Scott's reflexive domain in \(P\omega \) ⋮ Stochastic \(\lambda\)-calculi: an extended abstract ⋮ Towards Lambda Calculus Order-Incompleteness ⋮ Intersection Types and Computational Rules ⋮ On the ubiquity of certain total type structures ⋮ Completeness of intersection and union type assignment systems for call-by-value \(\lambda\)-models ⋮ Recursive Domain Equations of Filter Models ⋮ 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08 ⋮ Logical Semantics for Stability ⋮ Unnamed Item ⋮ Residuated structures and orthomodular lattices ⋮ Effective λ-models versus recursively enumerable λ-theories ⋮ Simple Easy Terms ⋮ Compositional characterisations of \(\lambda\)-terms using intersection types ⋮ Discrimination by parallel observers: the algorithm.

Cites Work

• Simple consequence relations
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• The system \({\mathcal F}\) of variable types, fifteen years later
• Realizability and recursive set theory
• Type theories, normal forms, and \(D_{\infty}\)-lambda-models
• Normal functors, power series and \(\lambda\)-calculus
• \(\mathbb{T}^\omega\) as a universal domain
• Sheaf models for set theory
• The lambda calculus, its syntax and semantics
• Algebras and combinators
• Domain theory in logical form
• Quantitative domains and infinitary algebras
• An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
• Representation of varieties in combinatory algebras
• A filter lambda model and the completeness of type assignment
• Isomorphisms and nonisomorphisms of graph models
• On the existence of extensional partial combinatory algebras
• The Category-Theoretic Solution of Recursive Domain Equations
• Data Types as Lattices
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item