Semantic Analysis of Definability and Normalisation for Typed Lambda

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.