Equivariant ZFA and the foundations of nominal techniques
arXiv:1801.09443 · doi:10.1093/logcom/exz015
Abstract
We give an accessible presentation to the foundations of nominal techniques, lying between Zermelo-Fraenkel set theory and Fraenkel-Mostowski set theory, and which has several nice properties including being consistent with the Axiom of Choice. We give two presentations of equivariance, accompanied by detailed yet user-friendly discussions of its theoretical significance and practical application.
References in corpus (6)
- Automata theory in nominal sets
- Nominal Unification from a Higher-Order Perspective
- PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
- From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
- Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
- Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness