Representation and duality of the untyped λ-calculus in nominal lattice and topological semantics, with a proof of topological completeness

We give a semantics for the λ-calculus based on a topological duality theorem in nominal sets. A novel interpretation of λ is given in terms of adjoints, and λ-terms are interpreted absolutely as sets (no valuation is necessary).