Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness
Publication:730088
DOI10.1016/J.APAL.2016.10.001zbMath1422.03023arXiv1305.5968OpenAlexW2964023069MaRDI QIDQ730088
Michael Gabbay, Murdoch James Gabbay
Publication date: 23 December 2016
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1305.5968
spectral spacesnominal algebraFraenkel-Mostowski set theoryfresh-finite limitslambda-reductionlattices and order
Lattices and duality (06D50) Other algebras related to logic (03G25) Combinatory logic and lambda calculus (03B40) Set-theoretic model theory (03C55)
Related Items (2)
Cites Work
- 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
- Lambda abstraction algebras: representation theorems
- A new approach to abstract syntax with variable binding
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- Capture-avoiding substitution as a nominal algebra
- A study of substitution, using nominal techniques and Fraenkel-Mostowksi sets
- Natural deduction and arbitrary objects
- Sheaves in geometry and logic: a first introduction to topos theory
- An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus
- On the algebraic models of lambda calculus
- Nominal unification
- Nominal rewriting
- A general mathematics of names
- On the representation theory for cylindric algebras
- Nominal Sets
- Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
- Towards nominal computation
- Freshness and Name-Restriction in Sets of Traces with Names
- Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax
- A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language
- A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing
- Stone Duality for Nominal Boolean Algebras with И
- Semantics Out of Context
- One-and-a-halfth-order Logic
- Capture-Avoiding Substitution as a Nominal Algebra
- A Nominal Axiomatization of the Lambda Calculus
- On universal algebra over nominal sets
- Applying Universal Algebra to Lambda Calculus
- A Formal Calculus for Informal Equality with Binding
- Nominal Algebra and the HSP Theorem
- Nominal (Universal) Algebra: Equational Logic with Names and Binding
- Pairing Without Conventional Restraints
- The lambda calculus is algebraic
- The virtues of eta-expansion
- Meta-variables as infinite lists in nominal terms unification and rewriting
- Explicit substitutions
- Topological representation of the λ-calculus
- Topological incompleteness and order incompleteness of the lambda calculus
- Innocent game models of untyped \(\lambda\)-calculus
This page was built for publication: Representation and duality of the untyped \(\lambda\)-calculus in nominal lattice and topological semantics, with a proof of topological completeness
