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. |
Mardi 4 Juillet
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Random generation of closed lambda-terms |
Description: |
Maciej Bendkowski |
Vendredi 7 Juillet
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Partiality and container monads |
Description: |
Niccolò Veltri We investigate monads of partiality in Martin-Löf type theory, following Moggis general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this talk, we unveil the relation between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolinis notion of dominance. We provide several examples, putting particular emphasis on Caprettas delay monad and its quotiented variant, the non-termination monad. |
Mardi 11 Juillet
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Sur le diamètre des polytopes en nombres entiers |
Description: |
Lionel Pournin |
Mardi 18 Juillet
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
clôture de cette année de séminaires & exposés de stagiaires |
Heure: |
14:30 - 17:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Roger Apéry et l'irrationalité de zêta(3) |
Description: |
Youssef Abdelaziz |
Heure: |
15:00 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Arbres de synchronisation et théorie de la concurrence |
Description: |
Medhi Naima |
Mercredi 30 Août
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Coherence for skew near-semiring categories |
Description: |
Tarmo Uustalu We consider skew near-semiring categories, a relaxation of near-semiring categories where the unitors, associators, annihilator and distributor are not required to be natural isomorphisms, they are just natural transformations in a particular direction. We prove a coherence theorem for such categories. The theorem states that, in a free skew near-semiring category over a set of objects, any two maps between an object and an object in normal form are equal.
Our main motivating examples for skew near-semiring categories are from programming with effects. While (relative) monads and lax monoidal functors are the same as skew monoids in particular skew monoidal categories, (relative) MonadPlus and Alternative instances are skew near-semiring objects.
This is joint work with Mauro Jaskelioff, Exequiel Rivas and Niccolò Veltri. |
|
|