Salut, Valentin n'étant pas encore arrivé (un peu juste en temps depuis GdN), on commencera plutôt à 11h30. Flavien Le 2017-06-06 12:14, breuvart a écrit :
AN INTERPRETATION OF SYSTEM F THROUGH BAR RECURSION
Valentin Blot, Queen Mary University of London
Salle B107, bâtiment B, Université de Villetaneuse
09/06/2017 11:00 - 12:30
Résumé : 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.
_______________________________________________ Gdtlogprog mailing list Gdtlogprog@lipn.univ-paris13.fr https://www-lipn.univ-paris13.fr/mailman/listinfo/gdtlogprog