Vendredi 17 Avril

Retour à la vue des calendrier
Vendredi 17 Avril
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: gdt Homotopy Type Theory - séance 1
Description: Andrew Polonsky The first of a little series of talks on Homotopy Type Theory (i.e., higher-order algebraic treatment of the notion of equality in dependant type theory).

Logical relations are a technique for proving meta-theoretic
properties of type systems.
In recent years, they have received a lot of attention as it became
clear that logical relations give the most natural definition of
extensional equality in type theory.
A major open problem is to define a type system which contains
extensional equality as an internal type constructor. For this, it is
necessary to reflect the external logical relation back into the
syntax of the type language.
In this talk I will describe how to do this.