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