Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
arXiv:1305.5968
Abstract
We give a semantics for the lambda-calculus based on a topological duality theorem in nominal sets. A novel interpretation of lambda is given in terms of adjoints, and lambda-terms are interpreted absolutely as sets (no valuation is necessary).