5 Juin - 11 Juin


Retour à la vue des calendrier
Vendredi 9 Juin
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: An interpretation of system F through bar recursion
Description: Valentin Blot There are two possible computational interpretations of second-order
arithmetic: Girard's system F or Spector's bar recursion and its
variants. While the logic is the same, the programs obtained from these
two interpretations have a fundamentally different computational
behavior and their relationship is not well understood. We make a step
towards a comparison by defining the first translation of system F into
a simply-typed total language with a variant of bar recursion. This
translation relies on a realizability interpretation of second-order
arithmetic. Due to Gödel's incompleteness theorem there is no proof of
termination of system F within second-order arithmetic. However, for
each individual term of system F there is a proof in second-order
arithmetic that it terminates, with its realizability interpretation
providing a bound on the number of reduction steps to reach a normal
form. Using this bound, we compute the normal form through primitive
recursion. Moreover, since the normalization proof of system F proceeds
by induction on typing derivations, the translation is compositional.
The flexibility of our method opens the possibility of getting a more
direct translation that will provide an alternative approach to the
study of polymorphism, namely through bar recursion.