# 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