Polarised realizability structures, models, and depolarisation

Guillaume Munch-Maccagnoni

(University of Cambridge)

Polarisation describes the presence of an evaluation order, and is
characterised denotationally by a non-associativity of compositions.
We recently proposed a polarised, Curry-style approach to the lambda-calculus
with extensional sums, in correspondence with polarised intuitionistic
logic. We suggested that associativity of composition in this context
should not be seen as a syntactic axiom, but as an emergent property
akin to termination. Traditionally, issues with sums in denotational
semantics have rather been considered to be with extensionality than
with the associativity. This will be explained in an introductory fashion in
a first part.

In a second part, I will more formally relate the termination in the
lambda-calculus with sums to depolarisation, i.e. associativity of
composition, or more familiarly the fact that the order of evaluation
does not matter. First, a general setting of polarised realizability
structures for polarised calculi with or without control operators is developed.
Then, a general technique to build observational models from these
structures is explained. Finally, under broad conditions, the observational
models that the non-associative syntactic structure gives rise to satisfy
the associativity of composition (and are therefore cartesian closed
categories with binary co-products). I will sketch an analogy between
intuitionistic depolarisation and parametricity.

Tuesday 27th October 2015, 13:15
Callahan 222 (via 218)
Department of Computer Science