Vendredi 21 Mars
Heure: 
10:00  12:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Can Dialectica break bricks? 
Description: 
PierreMarie 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 CurryHoward interpretation. We will fill this hole by presenting the computational content of Dialectica by means of an untyped lambdacalculus 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 dependentlytyped system almost without adaptation, thus giving a hindsight on how linear dependent types may be built (or not). 

