Mardi 1 Avril
Heure: |
14:15 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Sur la structure palindromique des mots |
Description: |
Srecko Brlek En combinatoire des mots finis ou infinis, la nature des motifs qui apparaissent dans un mot donné sont une des nombreuses manières de déterminer sa complexité. Les calculs de diverses statistiques permettent de mettre en évidencecertaines relations qu'il vérifie. |
Vendredi 4 Avril
Heure: |
10:00 - 11:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
De la charactérisation des modèles de H* |
Description: |
Flavien Breuvart Je donnerais une caractérisation (pour une large classe de model du lambda calcul pur) des modèles qui sont pleinement adéquat pour la normalisation de tête, càd dont la théorie est H*. Un K-model extentionel D est pleinement adéquat sii il est hyperimmune, càd que les comportements mal fondés ne sont pas capturées par aucun terme récursif. |
Heure: |
10:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
A Core Quantitative Coeffect Calculus |
Description: |
Aloïs Brunel Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this talk, we present a language, called lRPCF, inspired by a generalized interpretation of the exponential modality of bounded linear logic. In lRPCF exponential modalities carry a label--an element of a semiring--providing additional information on how a program uses its context. This additional information is used to express comonadic type analysis. |
Mardi 8 Avril
Heure: |
12:00 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Split Cuts and Separable Underestimator for non-convex quadratic problems |
Description: |
Emiliano Traversi In this work we investigate the computational potential of two tools for solving non-convex quadratic problems: split inequalities and separable underestimator. Split inequalities were first introduced by Letchford and further examined by Burer and Letchford. For small instances with box-constraints, we show that the resulting dual bounds are very tight.The gap can be further decreased by separating so-called non-standard split inequalities, which we examine in the case of ternary variables.Separable underestimator are used for solving constrained quadratic binary programming. Dual bounds are computed by choosing appropriate underestimators of the objective function that are separable but not necessarily convex. We explain how to embed this approach into a branch-and-bound algorithm and present experimental results for several classes of combinatorial optimization problems, including the quadratic shortest path problem, for which we provide the first exact approach available in the literature. |
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Réunion des CS pour audition MdC et Prof |
Jeudi 10 Avril
Heure: |
10:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Behavior driven design for tests and verification |
Description: |
Ulrich Kühne In the course of an exploratory project on hardware and system design and verification, we are looking for new ways how to bridge the gap between early abstract models and later implementation phases. One possible approach is the adaptation of agile techniques to the hardware domain, enhanced by model checking techniques. While in the design of hardware systems, testing and verification are usually applied as a post-process, software developement is pushed towards agile techniques like Test Driven Development (TDD), where tests play a central role. Behavior driven development (BDD) extends TDD as a well established software development technique. Essentially, in both techniques testing and implementing is interleaved, with the test cases being written first. In BDD, test cases are written in natural language which enables the discussion with stakeholders and easy requirements tracking throughout the design. In this talk, I will present a BDD tool for the Verilog hardware design language, which extends BDD with formal techniques. From test cases, properties can be generalized, making the verification more reliable, without the need to manually specify temporal properties. |
Vendredi 11 Avril
Heure: |
10:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Hypercoherence Spaces form a double-glued Category |
Description: |
Hugh Steele Ehrhard's Hypercoherence Spaces proved a useful medium through which to study strongly stable semantics. The category of hypercoherence spaces (HypCoh) has also been shown to be the bedrock of one of the very few fully complete models of unit-free multiplicative additive linear logic, satisfying Joyal's softness condition. Much like in the category of coherence spaces (Coh), an object of HypCoh is a set equipped with a collection of its subsets, with morphisms being relations respecting restrictions set by these `cliques'. However, unlike Coh, HypCoh has not been formalised as a true double-glued category.
In this talk I show that HypCoh is indeed such a category (if you're willing to bend the rules a little!). We also see how far the spirit of the glueing construction may be generalised to produce categories with similar properties. |
Mardi 15 Avril
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Some algebraic structures on chip firing game |
Description: |
Ha Duong Phan The chip firing game is a discrete dynamical model ongraphs which was first defined by D. Dhar (1990) and by A. Björner, L.Lovasz and W. Shor (1991). The model has various applications in manyfields of science such as physics, computer science, social science andmathematics. Recently, this model is used as a tool to study manyproperties of graphs and it was proved to be related to subjects of graphtheory, such as Laplacian matrix, Tutte polynomial, spanning tree orgraphic matroid, etc. In this talk, I will present some algebraicstructure raised on this model. |
Samedi 26 Avril
Heure: |
10:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Unification and Logarithmic space |
Description: |
Marc Bagnol I will present an algebraic characterization of the complexity classes Logspace and NLogspace, using an algebra with a composition law based on unification. This bridge between unification and complexity classes is inspired from proof theory and more specifically linear logic and Geometry of Interaction. |
Mardi 29 Avril
Heure: |
00:00 - 03:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
exposés ANR Magnum à P6: O. Bodini & A. Sportiello |
|
|