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

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).