Calculi

Marcelo Fiore

In this talk I will study normalisation for simply typed lambda

calculi with products and sums. I will start by analysing the
lambda

definability result of Jung and Tiuryn via Kripke logical relations

and show how it can be adapted to yield an extensional normalisation

result. I will then refine this later analysis by considering

intensional Kripke logical relations (in the form of glueing) and show

how they can be used to define a function for normalising terms,

providing thus normalisation by evaluation via glueing. Finally,
if

time allows, I will also present an extensional normalisation result

in the presence of sum types (via the more general Grothendieck

logical relations) and apply it to the categorical version of Tarski's

high school algebra problem.