2016


Retour à la vue des calendrier
Mardi 12 Janvier
Heure: 12:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: An Exact Semidefinite Programming Approach for the Max-Mean Dispersion Problem
Description: Michele Garraffa This work proposes an exact algorithm for the Max-Mean Dispersion Problem (Max-Mean DP), an NP-hard combinatorial optimization problem whose aim is to select the subset of a set such that the average distance between elements is maximized. The problem admits a natural non-convex quadratic fractional formulation from which a semidefinite programming (SDP) relaxation can be derived. In general, semidefinite relaxations have been successfully used to determine tight (but usually computationally expensive) lower/upper bounds for challenging NP-hard problems, such as the Quadratic Assignment Problem and the Quadratic Knapsack Problem. The semidefinite relaxation for the Max-Mean DP can be further tightened by means of a cutting plane algorithm which iteratively adds the most violated triangular inequalities. The proposed approach embeds the SDP relaxation and the cutting plane algorithm into a branch and bound framework to solve Max-Mean DP instances to optimality. To authors' knowledge, this is the first exact algorithm that has been proposed for this problem. Computational experiments show that the proposed method is able to solve to optimality in reasonable time instances with up 100 elements, while standard methods for fractional combinatorial optimization manage instances whose size is less then or equal to 75. The presented approach can be generalized to other combinatorial problems with a quadratic fractional objective and linear constraints.
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: TBC
Description: Julien Courtiel
Mercredi 13 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: TBC [attention, c'est un mercredi]
Description: Julien Courtiel
Lundi 18 Janvier
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Deep lexical segmentation and syntactic parsing in the easy-first dependency framework
Description: Joseph Le Roux
Jeudi 21 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: The CRT is the scaling limit of large random dissections
Description: Bénédicte Haas
Heure: 14:30 - 17:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: L'opération de flip dans les triangulations : du stockage de données à la topologie des surfaces
Description: Lionel Pournin
Jeudi 28 Janvier
Heure: 12:15 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Non negative matrix factorization for transfer learning
Description: Ievgen Redko The ability of a human being to extrapolate previously gained knowledge
to other domains inspired a new family of methods in machine learning
called transfer learning. Transfer learning is often based on the assumption
that objects in both target and source domains share some common feature
and/or data space. If this assumption is false, most of transfer learning
algorithms are likely to fail. In this work, we propose to investigate the
problem of transfer learning from both theoretical and applicational points
of view.

First, we introduce a theoretical framework based on the Hilbert-Schmidt
embeddings that allows us to improve the current state-of-the-art theoretical
results on transfer learning by introducing a natural and intuitive
distance measure with strong computational guarantees for its estimation.
The proposed results combine the tightness of data-dependent bounds derived
from Rademacher learning theory while ensuring the efficient estimation
of its key factors.

We also present two different methods to solve the problem of unsupervised
transfer learning based on Non-negative matrix factorization techniques.
First one represents a linear approach that aims at discovering
an embedding for two tasks that decreases the distance between the corresponding
probability distributions while preserving the non-negativity
property. Second one proceeds using an iterative optimization procedure
that aims at aligning the kernel matrices calculated based on the data from
two tasks.
Mardi 2 Février
Heure: 12:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: A Tabu Search Heuristic for a Staff Scheduling Problem
Description: Stefania Pan Scheduling problems form a very large class of optimization problems en-
countered in several industries and organizations of widely different kinds. The
particular problem that we consider is a staff scheduling problem, which con-
sists of assigning activities to employees by taking into account workload re-
quirements and different other constraints (for instance legal, economic, or-
ganizational and social constraints). Staff scheduling problems are NP-hard,
heuristics methods are often used to deal with large scale practical problems.
We focus on constraints which impose minimum and maximum duration on
activities. These constraints make the problem difficult to solve. We propose a
Tabu Search (TS) approach to deal with the specific staff scheduling problem
taking into account workload requirements and activities duration constraints.
Computational results show the effectiveness of the proposed approach compar-
ing CPLEX solver.
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Generating series of the trace group, and Möbius inversion
Description: Anne Bouillard
Mardi 9 Février
Heure: 12:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Primal Heuristics for Branch-and-Price
Description: Francois Vanderbeck Math heuristics have become an essential component in mixed integer programming (MIP) solvers. Extending generic MIP heuristics, our study outlines generic procedures to build primal solutions in the context of a Branch-and-Price approach and reports on their performance. Rounding the linear relaxation solution of the Dantzig-Wolfe reformu-lation, which is typically tighter than that of the original compact formulation, sometimes produces better solutions than state-of-the-art specialised heuristics as revealed by our numerical experiments. We focus on the so-called diving methods and their combination with diversification-intensification paradigms such as Limited Discrepancy Search, sub-MIPing, relaxation induced neighbourhood search, local branching, and strong branching. The dynamic generation of variables inherent to a column generation approach requires specific adaptation of heuristic paradigms. Our contribution lies in proposing simple strategies to get around these technical issues. Our numerical results on Generalized Assignment, Cutting Stock, and Vertex Coloring problems sets new benchmarks, highlighting the performance of diving heuristics as generic procedures in a column generation context.
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: TBC
Description: Nicolas Basset
Jeudi 11 Février
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Timed Aggregate Graph : a finite graph for model checking of Time Petri Nets
Description: Amal Chamakh Time Petri Nets (TPNs) are one of the most powerful formalisms for the
specification and the verification of systems involving explicit timing
constraints. To deal with model checking of timed systems modeled by TPNs, we
propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting
the behavior of bounded TPNs with strong time semantics. The main feature of
this abstract representation compared to existing approaches is the encoding
of the time information. This is done in a pure way within each node of the
TAG allowing to compute the minimum and maximum elapsed time in every path of
the graph. The TAG preserves timed traces and reachable states of the
corresponding TPN and allows for on-the-fly verification of reachability
properties. We also introduce an algorithm for a modular construction of the
TAG, to better confine the state explosion problem.
Vendredi 12 Février
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Hacking Nondeterminism with Induction and Coinduction
Description: Damien Pous Finite automata are used in a wide range of verification problems.
We introduce "bisimulation up to congruence" as a technique for
proving language equivalence of non-deterministic finite automata.
Exploiting this technique, we devise an optimisation of the classical
algorithm by Hopcroft and Karp which, as we show, is exploiting a
weaker "bisimulation up to equivalence" technique. The resulting
algorithm can be exponentially faster than the recently introduced
"antichain algorithms".
Mardi 16 Février
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: TBC
Description: Benjamin Hellouin
Jeudi 18 Février
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Sampled Weighted Min-Hashing for Large-Scale Topic Mining
Description: Ivan Vladimir MEZA Sampled Weighted Min-Hashing (SWMH) is a randomized approach to automatically mine topics from large-scale corpora. SWMH generates multiple random partitions of the corpus vocabulary based on term co-occurrence and agglomerates highly overlapping inter-partition cells to produce the mined topics. While alternative approaches define a topic as a probabilistic distribution over the complete vocabulary, SWMH topics are subsets of such vocabulary. Interestingly, the topics mined by SWMH underlie themes from the corpus at different levels of granularity. We extensively evaluate the meaningfulness of the mined topics both qualitatively and quantitatively on the NIPS (1.7K documents), 20 Newsgroup (20K), Reuters (800K) and Wikipedia (4M) corpora.
Vendredi 19 Février
Heure: 11:00 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Relational type-checking of connected proof-structures
Description: Luc Pellissier It is possible to define a typing system for Multiplicative Exponential Linear Logic (MELL): in such a system, typing judgments are of the form ? R : x : ?, where R is a MELL proof-structure, ? is the list of types of the conclusions of R, and x an element of the relational interpretation of ?, meaning that x is an element of the relational interpretation of R (of type ?).
As relational semantics can be used to infer execution properties of the proof-structure, these judgment can be considered as forms of quantitative typing.
We provide an abstract machine that decides, if R satisfies a geometric condition, whether the judgment ? R : x : ? is valid. Also, the machine halts in bilinear time in the sizes of R and x.
Mardi 1 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Algèbre de Hopf cambrienne
Description: Grégory Châtel En 1998, Loday et Ronco décrivent une algèbre de Hopf combinatoire dont la base est indicée par des arbres binaires. Cette algèbre possède de nombreux liens avec divers résultats antérieurs. Son produit est en particulier lié aux intervalles du treillis de Tamari, structure d'ordre partiel dont les éléments sont des arbres binaires. En 2006, Reading définit la notion de treillis cambrien d'un groupes de Coxeter. Le treillis Cambrien généralise l'ordre de Tamari en utilisant des structures arborescentes qui généralisent les arbres binaires : les arbres cambriens. Une question naturelle se pose alors : est-il possible de généraliser l'algèbre de Hopf de Loday-Ronco aux arbres cambriens ? Dans cette présentation, j'expliquerai les résultats que nous avons obtenus avec Vincent Pilaud sur les arbres cambriens en type A.
Jeudi 3 Mars
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Parameter Synthesis for Parametric Interval Markov Chains
Description: Laure Petrucci Interval Markov Chains (IMCs) are the base of a classic probabilistic specification theory introduced by Larsen and Jonsson in 1991. They are also a popular abstraction for probabilistic systems. In this paper we study parameter synthesis for a parametric extension of Interval Markov Chains in which the endpoints of intervals may be replaced with parameters. In particular, we propose constructions for the synthesis of all parameter values ensuring several properties such as consistency and consistent reachability in both the existential and universal settings with respect to implementations. We also discuss how our constructions can be modified in order to synthesise all parameter values ensuring other typical properties. Joint work with Benoît Delahaye and Didier Lime
Vendredi 4 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Caractérisation impérative des algorithmes séquentiels en temps quelconque, primitif récursif et polynomial
Description: Yoann Marquer Les fonctions calculables ont été formalisées par différents modèles de calcul (récursion, lambda-calcul, machines de Turing) ayant le même comportement entrées-sortie : c'est la thèse de Church. Par exemple, une machine de Turing à un ruban peut simuler les résultats calculés par une machine à deux rubans. Pourtant, pour la reconnaissance de palindrome la machine à un seul ruban nécessite une complexité en temps supérieure. Ainsi, il faut étudier les étapes intermédiaires. Nous définissons donc une simulation pas à pas entre exécutions, utilisant uniquement des variables temporaires et une dilatation temporelle.


La thèse de Church concernait donc les fonctions, et il nous faut une nouvelle thèse pour les algorithmes. Nous avons choisi celle de Gurevich pour sa présentation axiomatique : un algorithme séquentiel est un objet vérifiant les trois postulats de temps séquentiel, d'états abstraits et d'exploration bornée. De plus, il a montré que les algorithmes séquentiels coïncident avec son modèle des Abstract State Machines. Nous dirons donc qu'un modèle de calcul est algorithmiquement complet s'il existe une simulation mutuelle d'exécutions entre lui et les ASMs.


Pour obtenir des résultats sur des modèles de calcul plus usuels, nous formalisons les langages impératifs par un système de transition. En étudiant leur sémantique opérationnelle pas à pas et en développant une notion de graphe d'exécution, nous montrons qu'une variante du langage While de Jones est algorithmiquement complète. Ce résultat étant à structures de données près, il correspond donc à une équivalence entre les structures de contrôle des ASMs et des langages impératifs. De plus, étant préoccupés par la faisabilité des algorithmes, nous montrons que les structures du premier ordre utilisées par Gurevich permettent bien d'implémenter les structures de données usuelles.


Notre soucis de la faisabilité nous a également conduit à étudier en terme de complexité implicite deux restrictions des ASMs : celles en temps primitif récursif (les opérations usuelles et terminales) et celles en temps polynomial (les exécutions réalistes). Nous montrons d'une part que si les structures de données sont également primitives récursives, alors une variante LoopC du langage Loop de Meyer et Ritchie est complète pour les algorithmes en temps primitif récursif. D'autre part, une restriction syntaxique LoopCstat de LoopC est complète pour les algorithmes en temps polynomial, sans restriction sur les structures de données et en caractérisant syntaxiquement le degré du polynôme.
Vendredi 11 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Interaction Graphs and Quantitative Semantics
Description: Thomas Seiller Interaction Graphs (IG) models were introduced as a generalisation of Girard’s Geometry of Interaction (GOI) constructions based on the interpretation of proofs as (finite, weigthed) graphs. Recent results use IG models to bring into vision a new relation between dynamic and denotational semantics.
The first contribution of this work is the definition of categories of triskells, which generalises both the bicategory of spans and the categories of matrices and arrays over a semiring (also known as categories of weighted relations). Secondly, it sheds light onto a new relationship between dynamic and quantitative denotational semantics for multiplicative linear logic (MLL), providing formal grounds to the claim that IG models are a quantitative generalisation of dynamic semantics, i.e. GOI and game semantics. Finally, this functor is shown to preserve not only the interpretation of proofs but also induced double-glueing refinements: it is shown to lift to a map from the double-glueing construction defining IG models to the double-glueing construction yielding coherence spaces. For this purpose, a very general notion of quantitative coherence spaces is introduced, and shown to model full linear logic.
Mardi 15 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Partitions d'entiers et groupes de Coxeter
Description: Mathias Pétréolle En 2009, Han a redécouvert et généralisé une identité due à Nekrasovet Okounkov, qui fait un lien entre d'un coté, les puissances de lafonction êta de Dedekind, et de l'autre les partages d'entiers et leurslongueurs d'équerres. Pour cela, il utilise la formule de Macdonald pourle système affine de racines de type A. Je montrerai comment, à l'aidede bijections, il est possible de démontrer des identités deNekrasov-Okounkov pour d'autres types de systèmes de racines (typeaffine C et D notamment), et je présenterai les nouvelles formules deséquerres qui en découlent.Dans une seconde partie, je présenterai la notion d'élémentscycliquement pleinement commutatifs dans les groupes de Coxeter, qui ontété introduits pour étudier une version cyclique d'un théorème deMatsumoto. Je montrerai ensuit comment, en utilisant la théorie desautomates finis, on peut démontrer que la série génératrice de ceséléments est une fraction rationnelle, quelque soit le groupe de Coxeterconsidéré.
Heure: 15:00 - 18:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Treillis cambriens et treillis de Tamari : graphes dirigés et groupes de Coxeter
Description: François Viard
Vendredi 18 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Open Call-by-Value
Description: Giulio Guerrieri The elegant theory of the call-by-value lambda-calculus relies on
weak evaluation and closed terms, that are natural hypotheses in
the study of programming languages. To model proof assistants,
however, strong evaluation and open terms are required, and it is
well known that the operational semantics of call-by-value becomes
problematic in this case, as first pointed out by Paolini and Ronchi
della Rocca. Here we study the intermediate setting—that we call
Open Call-by-Value—of weak evaluation with open terms, on top
of which Grégoire and Leroy designed the abstract machine of Coq.
Various calculi for Open Call-by-Value already exist, coming from
logical, semantical, or implementative points of view, each one with
its pros and cons. This paper presents a detailed comparative study
of their operational semantics. First, we show that all calculi are
equivalent from a termination point of view, justifying the slogan
Open Call-by-Value. Second, we compare their equational theories.
Third, we present a detailed quantitative analysis of the time cost
model. Four, we introduce a new simple abstract machine, and
prove it a reasonable implementation of Open Call-by-Value with
respect to its cost model. Along the way, there emerges a sharp
deconstruction of call-by-value evaluation and of the complexity of
its implementations.

(Joint work with Beniamino Accattoli)
Lundi 21 Mars
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Apprentissage partiel de dépendances syntaxiques et application au transfert cross-lingue
Description: Ophélie Lacroix L'apprentissage supervisé est largement utilisé dans le domaine du TAL mais requiert l'exploitation de données correctement annotées. Nous nous intéressons en particulier au cas de l'analyse syntaxique en dépendances et montrons qu'il est possible d'apprendre un analyseur par transition à partir de données partiellement annotées.
Ce procédé est notamment profitable dans le cas du transfert d'annotations cross-lingue pour lequel les informations syntaxiques (les dépendances) sont projetées d'une langue source (bien dotée) à une langue cible (peu dotée) via des liens d'alignements. Les données partiellement annotées générées à partir de cette méthode permettent d'appre ndre des analyseurs en dépendances pour les langues ciblées. Cette méthode simple de transfert obtient des performances qui rivalisent avec celles de méthodes état-de-l'art récentes, tout en ayant un coût algorithmique moindre.
Mardi 22 Mars
Heure: 12:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Combinatorial Optimization subject to PDE constraints
Description: Christoph Buchheim We investigate a class of optimal control problems where the control parameters are binary variables, which are supposed to be static and probably subject to combinatorial constraints. Additionally, the problem contains state constraints involving semi-linear elliptic partial differential equations (PDEs). As an example, the binary variables may correspond to the activation of given heat sources attached to a metal sheet, the optimization problem then consists in switching on the smallest number of heat sources such that the point-wise temperature of the metal sheet is in a specified range. Our main result is that each state is a concave function in the binary control vector. This allows us to define an outer approximation scheme in which we alternate between the solution of a non-linear PDE and an integer linear program. Using this approach, we can solve instances on up to 2000 binary variables to global optimality.
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Calculer dans un automate cellulaire unidirectionnel réversible : vers l'indécidabilité de la périodicité?
Description: Martin Delacourt On s'intéresse au parallèle entre 2 problèmes sur des modèlesdistincts d'automates. D'une part, les automates de Mealy(transducteurs lettre à lettre complets) qui produisent dessemi-groupes engendrés par les transformations sur les mots infinisassociées aux états. En 2013, Gillibert a montré que le problème de lafinitude de ces semi-groupes était indécidable. En revanche laquestion est ouverte dans le cas où l'automate de Mealy produit un groupe. D'autre part, les automates cellulaires unidirectionnels pourlesquels la question de la décidabilité de la périodicité est ouverte.On peut montrer l'équivalence de ces problèmes. On fera un pas dans cette étude en montrant qu'il est possible desimuler du calcul Turing dans un automate cellulaire unidirectionnelréversible, rendant ainsi des problèmes de prédiction indécidablesainsi que la question de la périodicité partant d'une configuration finie.
Heure: 15:00 - 18:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Lattice paths in 3D
Description: Axel Bacher
Vendredi 25 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: String diagrams for Proof nets
Description: Matteo Acclavio Sequentialization of MELL proof nets needs additional tools extern to interaction nets syntax: connectivity, switchings, boxes and jumps. In this talk we introduce string diagrams syntax for monoidal categories in order to present a model for proof nets (with the relative cut elimination) with a unique local sequentialization criterion for MLL with constants and an idea for a generalization of this result for MELL proof nets.
Mardi 29 Mars
Heure: 10:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Regulated Grammars and Automata
Description: Alexander Meduna
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Lattice paths in 3D
Description: Axel Bacher
Heure: 15:00 - 18:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Regulated Grammars and Automata
Description: Alexander Meduna