Juin 2017


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.
Mardi 13 Juin
Heure: 10:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Opérades des cliques décorées
Description: Samuele Giraudo Nous proposons une construction fonctorielle de la catégorie des magmasunitaires vers celle des opérades non symétriques. Cette constructionmunit l'espace des configurations de diagonales décorées dans lespolygones d'une structure d'opérade. On obtient ainsi diverses nouvellesopérades sur des sous-familles particulières de tels polygones :configurations sans croisement, configurations non imbriquées,configurations de Motzkin, etc. Nous montrons aussi comment cetteconstruction permet de donner des définitions alternatives d'opéradesdéjà connues comme l'opérade des simples et doubles multi-tiles(provenant de la théorie des langages) et l'opérade de gravité.
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Séries génératrices généralisées via des opérades colorées et grammaires à bourgeons
Description: Samuele Giraudo
Vendredi 16 Juin
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Bar-récursion, analyse et réalisabilité classique
Description: Hadrien Batmalle
La réalisabilité classique est une théorie née des travaux de
Jean-Louis Krivine dans les années 1990, à la frontière entre la
logique et l'informatique théorique. Côté informatique, elle offre un
cadre adapté à l'interprétation calculatoire de preuves classiques.
Côté logique, elle apparaît comme une généralisation prometteuse du
forcing de Cohen. À un modèle du lambda-calcul, on peut ainsi associer
un modèle de la théorie des ensembles ZF.

On s'intéresse ici à des modèles de programmation vérifiant une
propriété de continuité: il peut s'agir de modèles basés sur les
domaines de la sémantique dénotationnelle, ou bien de modèles de
termes d'une version infinitaire du lambda-calcul. Dans ces modèles,
l'instruction 'quote' (qu'on utilise usuellement en réalisabilité
classique pour interpréter l'axiome du choix dépendant) n'est pas
disponible. On utilise donc la technique de la bar-récursion pour
interpréter l'axiome du choix dépendant. Or (en considérant la
réalisabilité classique comme une généralisation du forcing), il
apparaît que la bar-récursion est de plus l'analogue de la condition
de chaîne descendante dans les algèbres de forcing (qui correspond
à une propriété de préservation des réels). On obtient alors que toute
formule de l'analyse vraie dans le modèle ambiant est réalisée dans
ces nouveaux modèles, ce qui nous amène à la question suivante:
quel est le comportement des programmes réalisant des formules de
l'analyse?
Vendredi 23 Juin
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Petite introduction à la logique catégorique
Description: Damiano Mazza On entend dire parfois que le lambda-calcul est "le langage interne des catégories cartesiennes fermées". Le "langage interne" d'une catégorie est une notion très générale (mais, à vrai dire, pas tout à fait formelle) de logique catégorique. Dans cet exposé, j'introduirai les concepts de base pour comprendre cette notion et expliquer comment elle est reliée à la sémantique dénotationnelle.
Vendredi 30 Juin
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Inductive and Functional Types in Ludics
Description: Alice Pavaux Ludics is a logical framework in which types/formulas are modelled by sets of terms with the same computational behaviour. We investigate the representation of inductive data types and functional types in ludics. We study their structure following a game semantics approach. Inductive types are interpreted as least fixed points, and we prove an internal completeness result giving an explicit construction for such fixed points. The interactive properties of the ludics interpretation of inductive and functional types are then studied. In particular, we identify which higher-order functions types fail to satisfy type safety, and we give a computational explanation.