2017


Retour à la vue des calendrier
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 Moggi’s 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 Rosolini’s notion of
dominance. We provide several examples, putting particular
emphasis on Capretta’s 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