Vendredi 21 Mars

Retour à la vue des calendrier
Vendredi 21 Mars
Heure: 10:00 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Can Dialectica break bricks?
Description: Pierre-Marie Pédrot
The Dialectica translation is a logical transformation described by
Gödel in 1958, but designed in the 30's. At the end of the 80's, it was
given a categorical counterpart, which happened to be compatible with
the usual decomposition of intuitionistic logic into linear logic.
Still, it was lacking a true Curry-Howard interpretation.
We will fill this hole by presenting the computational content of
Dialectica by means of an untyped lambda-calculus translation. We will
show that this translation has a really simple explanation as soon as we
put our source term in the Krivine abstract machine, except for a
disturbing detail, seemingly deeply rooted in linear logic. We will also
show how our presentation can be naturally applied to a
dependently-typed system almost without adaptation, thus giving a
hindsight on how linear dependent types may be built (or not).