|
|
 |
|
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? |
|
|
