Pierre-Marie Pédrot: Can Dialectica Break Bricks?

Datum objave: 13. 4. 2015
Seminar za temelje matematike in teoretično računalništvo
Torek, 13. 4. 2015, od 12h do 14h, Plemljev seminar, Jadranska 19
Abstract: 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).