Topological nominal semantics
My longest ever paper was called "Representation and duality of the
untyped lambda-calculus" at nearly 91 pages.
Though too long, the paper does something unusual and interesting: we
build a topological semantics for the lambda-calculus, in which
lambda-calculus terms are given semantics as open sets in a
topological space, and lambda-abstraction becomes both a logical
quantifier and a corresponding operation on open sets.
A similar programme has also been carried out for first-order logic.
Taken together, these two papers show how to extend Stone duality from
(for example) Boolean algebras, to algebras for first-order logic and
the lambda-calculus. We can do this because we use nominal semantics
to handle the meaning of variables in first-order logic and the
This talk will not be an exhaustive technical account. Instead, I
will try to give an accessible overview of Stone-style duality theory,
and how and why new possibilities are opened up when looked at from
the point of view of nominal semantics. I will outline what
topological semantics look like in a nominal universe, and explain why
this is new and interesting.
Interested readers can view the two papers here:
"Representation and duality of the untyped lambda-calculus"
"Semantics out of context"
Journal of the ACM, 2016