Mardi 2 Mai
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Combinatoire énumérative des pseudo-n?uds |
Description: |
Jean-Marc Steyaert |
Heure: |
15:00 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Mots minimaux absents |
Description: |
Alice Héliou |
Vendredi 5 Mai
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Why complexity theorists should care about philosophy |
Description: |
Thomas Seiller Theoretical computer science was somehow born almost a hundred years ago when logicians asked themselves the question: "What is a computable function?". This question, purely theoretical, was answered before the first computer was designed, in the form of the Church-Turing thesis: a computable function is one that can be defined in one of the following equivalent models: recursive functions, Turing machines, or lambda-calculus. The apparition of actual computing devices however made it clear from the start that another question made more sense for practical purposes, namely: "What is an *efficiently* computable function?". This question was tackled by three different work in the span of a single year, marking the birth of computational complexity.
Nowadays, computational complexity is an established field: many methods and results have been obtained, and the number of complexity classes grows every year. However, a number of basic open problems remain unanswered, in particular concerning classification of complexity classes. Even worse than that, a number of results called barriers show that no known method will succeed in producing a new separation result, i.e. show that two classes (e.g. P and NP, or L and P) are disjoint. From a purely theoretical point of view, this lack of methods might be explained by a historic tradition of viewing programs as functions. Once this misconception identified, it points to a lack of adequate foundations for the theory of computation. Fortunately, some recent technical developments may provide a solution to this problem. |
Mardi 9 Mai
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Derivative-Free Line search Methods for Solving Integer Programming Problems |
Description: |
Francesco Rinaldi In this talk, we describe some derivative-free methods for integer programming problems with both bound constraints on the variables and general nonlinear c onstraints. The approaches combine linesearches with a specific penalty approach for handling the nonlinear constraints. The use of both suitable generated search directions and specific stepsizes in the linesearch guarantee that all the points are generated in the integer lattice.
We analyze the theoretical properties of the methods and show extensive numerical experiments on both bound constrained and nonlinearly constrained problems. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Random graphs and average-case analysis of NP-complete problems |
Description: |
Tom Denat |
Jeudi 11 Mai
Heure: |
12:15 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Accountable classification without frontiers |
Description: |
Khaled Belahcen We address the problem of multicriteria ordinal sorting through the lens of accountability, i.e. the ability of a human decision-maker to own a recommendation made by the system. We put forward a number of model features that would favor the capability to support the recommendation with a convincing explanation. To account for that, we design a recommender system implementing and formalizing such features. This system outputs explanations defined under the form of specific argument schemes tailored to represent the specific rules of the model. At the end, we discuss possible and promising argumentative perspectives. |
Vendredi 12 Mai
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Monades et comonades (suite) |
Description: |
Flavien Breuvart Dans cette deuxième séance du GdT modades et comonades, je présenterais les monades et comonades gradées. J'insisterais, en particulier, sur ma vision de ces objets comme potentielle piste pour faire interagir interprétation abstraite et typage dans les langages fonctionnels. |
Lundi 15 Mai
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Directed homology theories for geometric models of true concurrency |
Description: |
Jérémy Dubut Studying a system through its geometry is the main purpose of directed algebraic topology. This topic emerged in computer science, more particularly in true concurrency, where Pratt introduced his higher dimensional automata (HDA) in 1991 (actually, the idea of geometry of concurrency can be tracked down Dijkstra in 1965). Those automata are geometric by nature: every set of n processes executing independent actions can be modeled by a n-cube, and such an automata then gives rise to a topological space, obtained by glueing such cubes together, with a specific direction of time coming from the execution flow. It then seems natural to use tools from algebraic topology to study those spaces: paths model executions, homotopies of paths, that is continuous deformations of paths, model equivalence of executions modulo scheduling of independent actions, and so on, but all those notions must preserve the direction somehow. This brings many complications and the theory must be done again, essentially from scratch.
In this talk, after developing this idea of geometry of true concurrency, I will focus on homology. Homology is a nice computable tool from algebraic topology and it is a challenge in directed algebraic topology to find a satisfactory analogue that behaves well with direction. I will present our candidate of `directed homology, called natural (or bimodule) homology. This object consists in a functor with values in modules, which looks at the classical homology of trace spaces (a nice abstraction of what we may call `space of executions) and how those homologies evolve with time. This evolution can be studied through an abstract notion of bisimulation of functors with values in modules, that has many equivalent characterizations (using relations, using lifting properties, using Grothendieck construction,
) and whose existence is decidable in simple cases. Finally, among nice properties of our directed homology, I will show you that it is computable on simple spaces, which are already enough to model simple truly concurrent systems.
Joint work with Eric Goubault and Jean Goubault-Larrecq. |
Mardi 16 Mai
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Génération uniforme de marches 2D |
Description: |
Yann Ponty |
Heure: |
15:30 - 18:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Thé combinatoire accompagné d'un petit problème de combinatoire géométrique issu de l'apprentissage |
Description: |
Yann Chevaleyre |
Mardi 23 Mai
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Magouilles diverses pour les machines à signaux |
Description: |
Thierry Monteil Les machines à signaux sont un modèle de calcul déterministe dont espace et temps sont continus.Si les accumulations d'événements sont interdites, ce modèle est connupour être équivalent au modèle de BlumShubSmale linéaire. Nousconstruirons dans ce cadre un oracle universel optimal (en nombre devitesses et de paramètres irrationnels). Nous verrons comment jouer aubillard permet semi-décider l'algébricité d'un nombre réel alors que c'estimpossible dans le modèle BSS-linéaire. Nous verrons comment modifierlégèrement le modèle pour obtenir un modèle équivalent au modèle BSSstandard.Lorsque l'on permet aux accumulations d'événements de produire un signal,nous verrons, en jouant sur l'alternance discret/continu, commentconstruire des machines dont le pouvoir dépasse largement les modèles decalcul usuels, en particulier, nous construirons une "courbe de Peano" c'est a dire une surjection de [0,1] dans[0,1]^2. un "oracle universel continu", c'est à dire un machine à un paramètreM(p) telle que toute suite N->[0,1] est generèe un certain M(p). une "fonction analytique universelle", c'est à dire une machine avec2 parametres t,x telle que pour toute fonction analytique f de rayon deconvergence >1, il existe t tel que f(x)=M(t,x) pour tout x dans [-1,1],en particulier, on peut calculer les fonctions exp(x), sin(), en déplaçantun curseur. aussi, on peut prendre en compte la géométrie du modèle dans laformulation même de ce que peut "calculer" (ou "dessiner") une machine,pas seulement un booléen, un entier ou un réel comme dans le cas discret.Étant donnée une machine M, si certains types de collisions sont coloriésen rouge, l'ensemble de leurs accumulations au temps 1 est un compact. Ilse trouve que cette restriction est la seule : il existe une machine à unparametre M(p) telle que pour tout compact K inclus dans [0,1], il existep dans [0,1] tel que l'ensemble des accumulations rouges de M(p) au temps1 est K.L'exposé sera informel et sa compréhension ne nécessitera pas de prérequis. |
Mardi 30 Mai
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Combinatorial optimization problems in networks |
Description: |
Nelson Maculan We present optimization models with a polynomial number of variables and constraints for combinatorial optimization problems in networks: optimum elementary cycles (whose traveling salesman problem), optimum elementary paths even in a graph with negative cycles, and optimum trees (whose Steiner tree problem) problems. Computational results for the Steiner tree problem are also presented. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Sommes binomiales, diagonales de fonctions rationnelles et intégrales sur des cycles |
Description: |
Pierre Lairez |
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 |
|
|