Séminaires du LIPN
Depuis 2007, plus de 1059 séminaires ont été présentés dans le laboratoire

 Afficher les séminaires de tous les séminaires l'équipe A3 l'équipe AOC l'équipe CALIN l'équipe LCR l'équipe RCLN mercredi

Séminaires à venir
 04/03/2021 Titre bientôt disponible, par Kostia Chardonnet
 Kostia Chardonnet, LRI
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
04/03/2021    10:00 - 11:00
Résumé :
 05/03/2021 On the formal verification of safety-critical systems: challenges, approaches and perspectives, par Mohammed Foughali
 Mohammed Foughali, VERIMAG
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
05/03/2021    12:15 - 13:45
Résumé :
Safety-critical applications, e.g. those stemming from robotic, autonomous and cyber-physical systems, must be formally verified against crucial behavioral and timed properties. Yet, the use of formal verification techniques in such context faces a number of challenges, such as the absence of formal foundations of robotic frameworks and the lack of scalability of exhaustive verification techniques. In this talk, I will explore the approaches I have been proposing for the last six years to tackle these challenges, based on a global vision that favors correctness, user-friendliness and scalability of formal methods vis-à-vis real-world robotic and autonomous systems deployed on embedded platforms. I will discuss a major part of my work where safety-critical specifications are automatically translated into strictly equivalent formal models on which model checking, but also scalable non exhaustive techniques such as statistical model checking and runtime verification, may be used by practitioners to gain a considerable amount of trust in their underlying applications. Further, I will present a couple of techniques that allow to take into account hardware and OS specificities in the verification process, such as the scheduling policy and the number of processor cores provided by the platform, and thus increase the meaningfulness of the verification results. I will conclude with possible future research directions within the broad objective of deploying trustable safety-critical systems through bridging the gap between the software engineering, robotics, formal methods and real-time systems communities.
 05/03/2021 Contributions to Boolean satisfiability solving and its application to the analysis of discrete systems, par Souheib Baarir
 Souheib Baarir, LIP6 - Université de Paris Nanterre
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
05/03/2021    14:00 - 15:30
Résumé :
Despite its NP-Completeness, propositional (Boolean) satisfiability (SAT) covers a broad spectrum of applications. Nowadays, it is an active research area finding its applications in many contexts: planning decision, cryptology, computational biology, hardware and software analysis, etc. Hence, the development of approaches that could handle increasingly challenging SAT problems has become a focus. During these last 8 years, SAT solving has been the main subject of my research work, and in this talk I will present some of the main results we obtained in the field.
 11/03/2021 Learning to solve the single machine scheduling problem with release times and sum of completion times, par Axel Parmentier
 Axel Parmentier, ENPC
Salle B107, bâtiment B, Université de Villetaneuse
11/03/2021    10:30 - 11:30
Résumé :
In this work, we focus on the solution of a hard single machine scheduling problem by new heuristic algorithms embedding techniques from machine learning field and scheduling theory. These heuristics transform an instance of the hard problem into an instance of a simpler one solved to optimality. The obtained schedule is then transposed to the original problem. Computational experiments show that they are competitive with state-of-the-art heuristics, notably on large instances.
 17/03/2021 A snapshot of quantum algorithms for optimization, par Giacomo Nannicini
 Giacomo Nannicini, IBM - Watson
Salle B107, bâtiment B, Université de Villetaneuse
17/03/2021    15:00 - 16:00
Résumé :
There is much hype surrounding quantum computing and its potential applications for optimization. However, the technical details are often lost in translation. In this talk I will give an overview of quantum algorithms that may - one day - be useful for continuous and discrete optimization, highlighting possible sources of advantage as well as limitations. In particular, I will discuss variational hybrid algorithms for optimization, simulated annealing for counting problems, algorithms for linear systems, and algorithms for SDPs and LPs. I assume no prior knowledge of quantum mechanics.
 18/03/2021 Titre bientôt disponible, par Boris Eng
 Boris Eng, LIPN, Université Sorbonne Paris Nord
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
18/03/2021    10:00 - 11:00
Résumé :
 18/03/2021 Titre bientôt disponible, par Rim Saddem
 Rim Saddem
Salle A303
18/03/2021    14:00 - 15:00
Résumé :
 19/03/2021 Modeling and formal verification of a communicating autonomous vehicle system, par Johan Arcile
 Johan Arcile
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
19/03/2021    09:00 - 10:00
Résumé :
A system of autonomous vehicles consists of several agents individually making decisions in real time while exchanging information with other agents nearby. The validation of formal logic properties in such systems is not possible through naive approaches, due to the large number of variables involved in their representation. The two complementary works that will be presented have been developed to address this issue: - The VerifCar software framework, dedicated to decision-making analysis of communicating autonomous vehicles, which uses the state-of-art tool Uppaal. - The formalism of MAPTs and its dedicated exploration algorithms, allowing the use of heuristics that reduces the computation time needed to address reachability problems.
 01/04/2021 Titre bientôt disponible, par Marie Kerjean
 Marie Kerjean, LIPN, CNRS & Université Sorbonne Paris Nord
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
01/04/2021    10:00 - 11:00
Résumé :
 15/04/2021 Titre bientôt disponible, par Giulio Guerrieri
 Giulio Guerrieri, University of Bath
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
15/04/2021    10:00 - 11:00
Résumé :
Séminaires passés
 25/02/2021 [Séminaire Chocola] Titre bientôt disponible, par Zeinab Galal
 Zeinab Galal, IRIF, Université de Paris
http://chocola.ens-lyon.fr/events/online-2021-02-25/
25/02/2021    10:00 - 12:00
Résumé :
 18/02/2021 Combinatorial Optimization Theory and Algorithms for Set Packing and Location Problems, par Mercedes Pelegrin
 Mercedes Pelegrin, LIX
Salle B107, bâtiment B, Université de Villetaneuse
18/02/2021    10:30 - 11:30
Résumé :
In this talk, we will cover modeling for two optimization problems, as well as Mathematical Programming methods that can be applied to solve them. The first part will be devoted to the set packing problem, one of the seminal problems in Combinatorial Optimization. We will focus on generating hyperplanes to describe the set packing polytope. Namely, we will present a new lifting theorem and illustrate its application to facility location. In the second part of the talk, we will address the problem of identifying a group of key nodes in a network. We will propose a mixed integer nonlinear program (MINLP) that embeds eigenvector centrality in a clustering partition. The resulting model uncovers the group of key nodes (the clusters centroids) and their communities (the clusters). Modeling this idea involves nonlinear equations, which will be linearized to produce a mixed integer linear program (MILP). Symmetry breaking, a recurrent topic in Combinatorial Optimization, will be also addressed. Computational results on synthetic and real-life networks will be presented.
 18/02/2021 Enriched concurrent games: witnesses for proofs and resource analysis, par Aurore Alcolei
 Aurore Alcolei, Università di Bologna
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
18/02/2021    10:00 - 11:00
Résumé :
Game semantics is known as the semantics of control flow and interactions. Among its various models, causal game models emphasize the causal relation between the computational events that describe these interactions. This view point is particularly suitable to represent parallel computations and concurrent behaviours. In this talk I will show how causal game models can be enriched with annotations in order to capture side computations, that are, computational information that varies with the control flow but does not affect it. This enrichment will motivated through two semantics problems in both logics and programming: - Offering a novel compositional interpretation of Herbrand theorem by capturing the structure of Herband witnesses as causal strategies annotated with terms; - Enriching a sound and adequate concurrent game model for higher order concurrent programs with quantitative information in order to reflect their minimal execution time.
 11/02/2021 Linearization techniques for MINLP, par Sandra Ulrich Ngueveu
 Sandra Ulrich Ngueveu, LAAS-CNRS
Salle B107, bâtiment B, Université de Villetaneuse
11/02/2021    10:30 - 11:30
Résumé :
We review state-of-the-art linearization and approximation techniques for the solution of non-linear mixed-integer programs. We show in particular how to ensure an a priori guarantee on the quality/feasibility of the solution, a reduction of the size of the converted problem and a minimization of the computing time. We then present an iterative method for the solution of a class of non-linear mixed-integer programs to arbitrary numerical precision. By keeping the scope of the update local from one iteration to another, the computational burden is only slightly increased from iteration to iteration. As a consequence, our method presents very nice scalability properties and is little sensitive to the desired precision. We assess its efficiency for approximating the non-linear variants of three problems: the uncapacitated facility location problem, the multi-commodity network design problem, and the transportation problem. Our results indicate that, as the desired precision becomes smaller, our approach can lead to significant gains in computing times, often being orders of magnitude faster than a baseline method, and scales to approximate larger problems.
 11/02/2021 [Séminaire Chocola] Sequentiality, References and Well-bracketing in the pi-calculus, par Enguerrand Prebet
 Enguerrand Prebet, ENS Lyon
http://chocola.ens-lyon.fr/events/online-2021-02-11/
11/02/2021    10:00 - 12:00
Résumé :
The pi-calculus is used as a model for programming languages. Its contexts exhibit arbitrary concurrency, making them very discriminating. This may prevent validating desirable behavioural equivalences in cases when more disciplined contexts are expected. We formalise using types three different disciplines: sequentiality or the idea of having a single thread of computation ; reference types for which channels behave like bits of store or atomic register ; and well-bracketing which strengthens the sequentiality constraints to also obey a stack-like discipline. For each, we present the type system along with its consequences on behavioural equivalence and the corresponding bisimulation techniques.
 09/02/2021 Symbolic Verification Techniques for Multiparty Interaction, par Carlos Olarte
 Carlos Olarte, Federal University of Rio Grande do Norte (Brazil)
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
09/02/2021    12:00 - 13:00
Résumé :
Multiparty interactions are commonplace in today's distributed systems. An agent usually communicates, in a single session, with other agents to accomplish a given task. Take for instance an online transaction including the credit card system, the vendor and the client. What we observe is a single transaction composed of several (binary) interactions leading to changes in the state of all the involved agents. Multiway synchronization process calculi, that move from a binary to a multiparty synchronization discipline, have been proposed to formally study the behavior of those systems. For instance, the Core Network Algebra (CNA) extends the point-to-point communication discipline of Milner's CCS with link-chains, describing how information flows among the agents. In this model, the number of participants in an interaction cannot be fixed a priori, and hence, CNA computations are inherently non-deterministic. This leads to an exponential blow-up in the number of reachable states and makes it difficult to devise verification techniques for this formalism. In this talk, I will show four mechanisms that we have proposed for tackling this problem. Namely: (1) A symbolic semantics and bisimulation for CNA that are more amenable for automated reasoning. Symbolic configurations represent, compactly, a possibly infinite number of states and they can be effectively checked. (2) The Symbolic Link Modal Logic, a smooth extension of Hennessy-Milner logic that faithfully characterizes the (symbolic) transitions of CNA processes. (3) An extension of CNA with constraints that declaratively allow the modeler to restrict the interactions that should actually happen. Our definition of constraints is general enough, and it offers the possibility of accumulating costs in multiparty negotiations. This extension finds applications in the modeling of Service Level Agreement protocols and balancing the interactions in a concurrent system. (4) A suitable representation of the above techniques as an executable rewrite theory. Our implementation of this theory in Maude offers the possibility of animating CNA specifications, and it provides (automatic) verification procedures to analyze them.
 04/02/2021 A uniform framework for substructural logics with modalities , par Elaine Pimentel
 Elaine Pimentel, Universidad Federal del Rio Grande do Norte
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
04/02/2021    14:00 - 15:00
Résumé :
In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. (joint work with Björn Lellmann and Carlos Olarte).
 28/01/2021 Postier chinois dans les triangulations planaires et applications à la chimie, par Matej Stehlik
 Matej Stehlik, INP Grenoble
Salle B107, bâtiment B, Université de Villetaneuse
28/01/2021    10:30 - 11:30
Résumé :
Le problème du postier chinois est un problème classique de loptimisation combinatoire. Dans cet exposé, je me concentrerai sur le problème du postier chinois dans les triangulations planaires. Je montrerai une borne optimale sur la longueur du plus court parcours de postier, et je discuterai des liens à la chimie théorique.
 28/01/2021 [Séminaire Chocola] Stable Relations and Abstract Interpretation of Higher-Order Programs, par Benoît Montagu
 Benoît Montagu, INRIA
http://chocola.ens-lyon.fr/events/online-2021-01-28/
28/01/2021    10:00 - 12:00
Résumé :
We present a novel denotational semantics for the untyped call-by-value ?-calculus, where terms are interpreted as stable relations, i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its results---a form of frame condition for functional programs.
 26/01/2021 Vérification formelle de systèmes distribués et de leurs propriétés réseau, par Nicolas SCHNEPF
 Nicolas SCHNEPF
Salle A303
26/01/2021    12:00 - 13:30
Résumé :
Lemploi de méthodes formelles est aujourdhui plus que jamais nécessaire pour assurer la vérification ou la synthèse de politiques réseau assurant les propriétés de sûreté et de sécurité requises par les systèmes distribués contemporains. Dans cet exposé je présenterai mes travaux de thèse autour de lorchestration et de la vérification formelle de fonctions de sécurité pour des environnements intelligents tels que des smartphones ou des tablettes, après quoi jaborderai les résultats dun article récemment accepté à Tacas 2021 dans le cadre de mon postdoc portant sur la vérification quantitative de réseaux sous condition de pannes de liens. Finalement je présenterai les collaborations que jenvisage avec votre équipe, en particulier en termes de vérification modulaire darchitectures multi-protocoles mais également en termes dutilisation de méthodes formelles pour prouver les propriétés de sécurité darchitectures distribuées multi-agents ou encore pour détecter des applications malveillantes à plusieurs niveaux dobservation.
 21/01/2021 Extensional denotational semantics of probabilistic programs, beyond the discrete case, par Guillaume Geoffroy
 Guillaume Geoffroy, Università di Bologna
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
21/01/2021    10:00 - 11:00
Résumé :
The idea of extensional denotational semantics is to interpret first-order probabilistic programs as measure transformers. For example, a program that takes as input a handle to a random generator of real numbers and outputs a randomly chosen real number is interpreted as a map that takes a sub-probability measure on R and returns a sub-probability measure on R. Beyond first order, extensional means that each type is interpreted as a set with some additional structure, and programs as structure-preserving maps. The question of what structure exactly is a long-standing one. We will see in what way the structures that have been proposed so far are not completely satisfactory as soon as non-discrete probabilities are involved, why such a structure should at least include that of an algebra over the monad of sub-probability measures, and an example of structure that seems to fit the bill.
 14/01/2021 [Séminaire Chocola] Taylor Subsumes Scott, Berry, Kahn and Plotkin, par Giulio Manzonetto
 Giulio Manzonetto, LIPN, Université Sorbonne Paris Nord
http://chocola.ens-lyon.fr/events/seminaire-2021-01-14/
14/01/2021    10:00 - 12:00
Résumé :
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential lambda-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in lambda-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
 18/12/2020 On higher-order cryptography, par Raphaëlle Crubillé
 Raphaëlle Crubillé, LORIA
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 749983)
18/12/2020    15:15 - 16:15
Résumé :
Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes themselves higher-order? This work gives an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, then showing how the concept of probabilistic polynomial time algorithm can be generalized so as to encompass algorithms of order strictly higher than two, and finally proving some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions.
 17/12/2020 History-Dependent Nominal mu-Calculus, par Clovis Eberhart
 Clovis Eberhart , ERATO MMSD project, Tokyo
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
17/12/2020    10:30 - 11:30
Résumé :
The mu-calculus with atoms, or nominal mu-calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history. This is joint work with Bartek Klin.
 17/12/2020 Combinatorial Optimization problems in telecommunication networksitre bientôt disponible, par Sébastien Martin
 Sébastien Martin, NTO team from DataCom Department, Huawei Technologies Co.,Ltd.
Salle B107, bâtiment B, Université de Villetaneuse
17/12/2020    10:30 - 11:30
Résumé :
The telecommunication network area provides lot of interesting optimization problems. Furthermore, the arrival of 5G technology modifies the traditional combinatorial optimization problems by adding some specificities. We quickly present some case studies done by the "network optimization" team from "Datacom" department. For instance, we present the "network slicing technology" ensuring isolation in resource sharing among users. We also describe the "Deterministic Networking" to guarantee bounded jitter and latency constraints. Finally, we show how to consider network calculus in optimization problems to ensure latency guarantees. We finish by the presentation of future telecommunication network topics from an optimization point of view. Joint work with Nicolas Huin, Jérémie Leguay, Youcef Magnouche, Paolo Medagliani
 14/12/2020 Measurable Game Semantics, par Hugo Paquet
 Hugo Paquet, University of Oxford
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 749983)
14/12/2020    10:00 - 11:00
Résumé :
I will present recent work on a denotational semantics for probabilistic programs based on games and strategies. This is a probabilistic enrichment of concurrent games on event structures, a model extensively developed in the past few years by Winskel, Clairambault, Castellan and others. Concurrent games have been used successfully to model computation with discrete probability; applications include full abstraction results for probabilistic extensions of PCF and the pure lambda-calculus. I will focus on an extension of the above with measure-theoretic structure. The resulting category supports higher-order types, continuous probability distributions, and primitives for conditioning, and can be used to model both call-by-value and call-by-name.
 07/12/2020 wikiSERA: Domain independent evaluation of automatic summaries using relevance analysis on Wikipedia, par Jorge Garcia Flores
 Jorge Garcia Flores, LIPN
Salle B107, bâtiment B, Université de Villetaneuse
07/12/2020    12:30 - 13:30
Résumé :
Text summarization has been the subject of increasing research efforts in the last years. However, automatic summary evaluation is as crucial as the summarization task itself. For more than 15 years, the dominant approach for evaluating this task has been ROUGE [Lin, 2004], a machine translation inspired lexical comparison between a candidate machine summary and a set of human gold standard summaries. Lexical comparison might be a suitable evaluation approach for extractive summarization systems. However, the methodological leap of Deep Learning brought increasing research efforts on abstractive summarization, which raised some questions about the pertinence of an all-lexical evaluation perspective. In this work we present wikiSERA, an open source improvement of the SERA evaluation method [Cohan et al., 2018], based on a semantic comparison of information extraction vectors from a document base. We adapted the method to generic domain summarization and provide to the community a Wikipedia based implementation that shows robust correlation with human evaluations. --- Après le séminaire on va saluer Jorge qui nous quitte pour quelques mois, avec un apéro de "résistance" (contre la Covid, la LPR, etc..)
 03/12/2020 Geometric Set Cover via Randomized LP Rounding, par Mustafa Nabil
 Mustafa Nabil, ESIEE Paris and LIGM
Salle B107, bâtiment B, Université de Villetaneuse
03/12/2020    10:30 - 11:30
Résumé :
Geometric set-cover/hitting-set problems arise naturally in several basic settings, and therefore the problem of computing small set covers (and hitting sets) has been studied extensively. A common first step in solving such optimization problems is to formulate and solve the corresponding covering/packing LP to get a fractional solution. Then the task reduces to constructing an integer solution from this fractional solution. In this talk, I will present a new simple iterative randomized rounding scheme that gives optimal approximation bounds, within constant factors, for many well-studied geometric systems.
 26/11/2020 Émergence de nouveaux problèmes combinatoires pour les systèmes de production dans le contexte Industrie 4.0, par Paolo Gianessi
 Paolo Gianessi, EMSE - Saint-Etienne
Salle B107, bâtiment B, Université de Villetaneuse
26/11/2020    10:30 - 12:00
Résumé :
Du fait des nouveaux paradigmes de production imposés par l'Industrie 4.0 et de l'attention grandissante portée par l'opinion publique à l'égard des questions environnementales, les systèmes de production doivent relever le double défi de répondre à une demande de plus en plus variable mais aussi faire preuve d'une efficacité énergétique accrue. De nouveaux problèmes combinatoires ont ainsi commencé à paraître dans la littérature de l'Optimisation des systèmes de production à coté des problèmes plus traditionnels. Nous en présentons ici trois, que nous avons étudiés au cours de ces deux dernières années, et qui touchent à la planification stratégique ou tactique/opérationnelle: un problème d'ordonnancement de type job-shop avec prise en compte de l'énergie; un problème d'équilibrage de ligne avec minimisation du pic de puissance; et un problème bi-niveau d'équilibrage de ligne d'un RMS (système de production reconfigurable) visant à minimiser le coût de la consommation énergétique vis-à-vis d'un plan tarifaire donné. Ces problèmes ont pour l'instant été abordés par de premières approches simples (PLNE, méta-heuristiques par décomposition et/où recherche locale) afin d'en démontrer l'intérêt pratique auprès de la communauté industrielle; il paraît tout de même évident qu'ils offrent des développements potentiels à investiguer aussi d'un point de vue plus proprement algorithmique et combinatoire, et par conséquent s'affichent comme de nouveaux éléments d'intérêt certain de la frontière entre applications réelles et recherche fondamentale.
 26/11/2020 Quantitative Tauberian Theorems, par Thomas Powell
 Thomas Powell, University of Bath
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
26/11/2020    10:00 - 11:00
Résumé :
In this talk I seek to achieve two things. First, I aim to give a very concise introduction to modern applied proof theory, without assuming any prior knowledge of this area. Second, I will present some new reasearch of mine in Tauberian theory, which studies the convergence of different summation methods for infinite series.
 19/11/2020 A Tight Approximation Algorithm for the Cluster Vertex Deletion Problem, par Samuel Fiorini
 Samuel Fiorini, Université libre de Bruxelles
Salle B107, bâtiment B, Université de Villetaneuse
19/11/2020    10:30 - 11:30
Résumé :
We give the first 2-approximation algorithm for the cluster vertex deletion problem. This is tight, since approximating the problem within any constant factor smaller than 2 is UGC-hard. Our algorithm combines the previous approaches, based on the local ratio technique and the management of true twins, with a novel construction of a 'good' cost function on the vertices at distance at most 2 from any vertex of the input graph. As an additional contribution, we also study cluster vertex deletion from the polyhedral perspective, where we prove almost matching upper and lower bounds on how well linear programming relaxations can approximate the problem.
 19/11/2020 Introduction to Parametric Verification 2/2, par Laure Petrucci
 Laure Petrucci, LIPN, Université Sorbonne Paris Nord
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
19/11/2020    10:00 - 11:00
Résumé :
(Filled in by Thomas.) The talk will be the second of two sessions providing a short introduction to parametric verification of concurrent systems. Associated ArXiv paper: https://hal.archives-ouvertes.fr/hal-02170526.
 12/11/2020 Differentiating stateful processes, par David Sprunger
 David Sprunger, ERATO MMSD Project, Tokyo
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
12/11/2020    16:00 - 17:00
Résumé :
In this talk, we develop a notion of differentiation for Mealy machines with smooth transition functions. This notion of differentiation is based in the theory of Cartesian differential categories, a synthetic, categorical treatment of differentiation. We exhibit a construction augmenting any Cartesian differential category with a trace-like operation modeling internal state. We apply these categorical constructions to model recurrent neural networks, investigate compositional properties of their derivatives, and ultimately design improved training algorithms in machine learning. Joint work with Shin-ya Katsumata.
 05/11/2020 An exact algorithm for robust influence maximization, par Roberto Wolfler Calvo
 Roberto Wolfler Calvo, LIPN
Salle B107, bâtiment B, Université de Villetaneuse
05/11/2020    10:30 - 11:30
Résumé :
We propose a Branch-and-Cut algorithm for the robust influence maximization problem. The influence maximization problem aims to identify, in a social network, a set of given cardinality comprising actors that are able to influence the maximum number of other actors. We assume that the social network is given in the form of a graph with node thresholds to indicate the resistance of an actor to influence, and arc weights to represent the strength of the influence between two actors. In the robust version of the problem that we study, the node thresholds are affected by uncertainty and we optimize over a worst-case scenario within a given robustness budget. Numerical experiments show that we are able to solve to optimality instances of size comparable to other exact approaches in the literature for the non-robust problem, but in addition to this we can also tackle the robust version with similar performance.
 05/11/2020 Journée Opérades LIPN-LAGA, par Conférence
 https://operades20.sciencesconf.org 05/11/2020    09:30 - 16:00 Résumé : Le programme est disponible en ligne (https://operades20.sciencesconf.org). Pensez à vous inscrire sur le site pour recevoir les informations de connexion. Le premier exposé contiendra une introduction à la théorie des opérades. Liste des orateurs invités: Samuele Giraudo (LIGM, U. Gustave Eiffel), Guillaume Laplante-Anfossi (LAGA, U. Sorbonne Paris Nord), Maxime Lucas (LIPN, U. Sorbonne Paris Nord), Damiano Mazza (LIPN, CNRS).
 29/10/2020 Mathematical specifications of programming languages via modules over monads, par Ambroise Lafont
 Ambroise Lafont, Cogent team, University of New South Wales
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 749983)
29/10/2020    09:00 - 10:00
Résumé :
Research in the field of programming languages traditionally relies on a definition of syntax modulo renaming of bound variables, with its associated operational semantics. We are interested in mathematical tools allowing us to automatically generate syntax and semantics from basic data. We pay particular attention to the notion of substitution, using the categorical notions of monads and modules over them. Languages with variable binding, such as the pure lambda calculus, are monads on the category of sets. We provide a further notion of transition monads which takes into account the operational semantics. We give examples of specifications for transition monads, in the spirit of Initial Semantics, where an object is characterized by some initiality property in a suitable category of models.
 22/10/2020 Introduction to Parametric Verification 1/2, par Laure Petrucci
 Laure Petrucci, LIPN, Université Sorbonne Paris Nord
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
22/10/2020    10:00 - 11:00
Résumé :
(Filled in by Thomas.) The talk will be the first of two sessions providing a short introduction to parametric verification of concurrent systems. Associated ArXiv paper: https://hal.archives-ouvertes.fr/hal-02170526.
 15/10/2020 Interaction Laws of Monads and Comonads, par Exequiel Rivas
 Exequiel Rivas, Inria
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
15/10/2020    10:00 - 11:00
Résumé :
Since Moggi's seminal work, monads have been recognized as a way of capturing computational effects. Following this line, we take a view in which their dual, comonads, can be used to capture some form of environment that can interact with such computations. In this talk, we will present a categorical theory of interaction between monads and comonads, abstracting the execution of a computation in an environment. We will highlight connections to previous categorical constructions such as the Chu construction and gluing in the style of Hasegawa. This is joint work with Shin-ya Katsumata and Tarmo Uustalu.
 12/10/2020 Person-Independent Multimodal Emotion Detection for Children with High-Functioning Autism, par Annanda Sousa
 Annanda Sousa, Université de Galway (Irlande)
Salle B107, bâtiment B, Université de Villetaneuse
12/10/2020    12:30 - 14:00
Résumé :
The use of affect-sensitive interfaces carries the promise of enhancing human-computer interaction by delivering a system capable of identifying a user's emotions and adapt its content accordingly. Today's technology shows great potential to support children with autism, for example by using computer systems to improve their social skills. Generally, however, this technology does not encompass the potential of affect-sensitive interfaces. This is mainly due to Emotion Detection (ED) models built for the general population usually not performing well when applied to children with autism, who express emotions differently. The aim of this project is therefore to build a person-independent Multimodal Emotion Detection system tailored for children with high-functioning autism for the ultimate goal of applying it to design affect-sensitive interfaces dedicated to children with autism. This is a work in progress and the project expects to build upon the current body of knowledge on methods to apply ED systems to this specific subset of the general population. We expect to apply the overall theoretical and practical design perspectives that arise from this research investigation (e.g. analysis of modalities and features extraction, behavioural cues based features, fusion layers and classifier techniques) to propose a guiding framework for future studies.
 08/10/2020 On Higher-Order (In)Efficiencies, par Gabriele Vanoni
 Gabriele Vanoni, Università di Bologna
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
08/10/2020    10:00 - 11:00
Résumé :
Intersection types (IT) for the lambda-calculus extend simple types with an intersection operator. They are able to characterize crucial qualitative properties of programs, such as strong, weak and head normalization, and they have been extensively studied for their connections with models and semantics of programming languages. Moreover, considering a variation of the type system in which the intersection is non-idempotent, has led to new quantitative results and simplified many proofs, in the very same way linear logic did, i.e. taking into account the use of resources. This way, non-idempotent IT are able to characterize, for example, the number of steps Krivines machine needs to evaluate a term. We show how altering the way in which weights are assigned gives the number of steps the Interaction Abstract Machine (IAM) needs to evaluate a term. This way, we quantitatively observe that the inefficiencies of the IAM come from the presence of higher-order types in the IT derivation. This is joint work with Beniamino Accattoli and Ugo Dal Lago.
 01/10/2020 Cons-free programs for functional complexity classes, par Siddharth Bhaskar
 Siddharth Bhaskar, DIKU, University of Copenhagen
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
01/10/2020    10:00 - 11:00
Résumé :
The "cons-free programs" of Neil Jones, in which data can be destructed but not constructed, capture relational LOGSPACE or PTIME over strings, depending on whether we allow tail recursion or general recursion. By generalizing cons-free programs to "RW-factorizable programs," in which there are separate construct-only and destruct-only data types, we recover functional LOGSPACE and PTIME over strings. This seems to be a novel implicit characterization of these classes. RW-factorizable programs faithfully express several natural algorithms. In particular, we study RW-factorizable comparison sorting, prove a quadratic lower bound on the running time of all such sorting programs, and show that this is tight. Finally we conclude with some thoughts about a program for "comparative implicit computational complexity," based on studying indexings of complexity classes obtained from various implicit characterizations.
 28/09/2020 Recherche dexperts à partir de publications scientifiques, par Stella Zevio
 Stella Zevio, LIPN
Salle B107, bâtiment B, Université de Villetaneuse
28/09/2020    12:30 - 13:30
Résumé :
Qui assigner au comité de lecture de la conférence que j'organise ? Au comité de thèse de mon doctorant ? Qui sont les membres éminents et les publications phares de mon domaine de recherche ? Suis-je un chercheur émérite ? Qui dois-je citer et avec qui dois-je collaborer pour espérer faire partie des membres éminents de la communauté scientifique et améliorer ma réputation ? Afin de répondre à ces problématiques essentielles, nous proposons une méthode de recherche dexperts à partir de publications scientifiques combinant annotation sémantique à laide dune ontologie et fouille de motifs dans les coeurs de graphes attribués.
 24/09/2020 Intersection Type Distributors, par Federico Olimpieri
 Federico Olimpieri, Aix-Marseille Université
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
24/09/2020    10:00 - 11:00
Résumé :
Building on previous works, we present a general method to define proof relevant intersection type semantics for pure lambda calculus. We argue that the bicategory of distributors is an appropriate categorical framework for this kind of semantics. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management, following Marsden-Zwardt's approach. We show how these monadic constructions determine Kleisli bicategories over the bicategory of distributors and we give a sufficient condition for cartesian closedness. We define a family of non-extentional models for pure lambda calculus. We then prove that the interpretation of lambda terms induced by these models can be concretely described via intersection type systems. The intersection constructor corresponds to the particular tensor product given by the considered free monadic construction.
 17/09/2020 All your base categories are belong to us: A syntactic model of presheaves in type theory, par Pierre-Marie Pédrot
 Pierre-Marie Pédrot, INRIA
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
17/09/2020    10:00 - 11:00
Résumé :
Presheaves are a staple categorical structure, which naturally arises in a wide variety of situations. In the realm of logic, they are often used as a model factory. Indeed, presheaves over some base category will result in a topos, whose contents can be fine-tuned by carefully picking the base category. As computer scientists, though, we have learnt that there are even better logical systems than toposes: dependent type theories! Through the Curry-Howard mirror, they are also full-blown functional programming languages that actually compute. This begs the following question: is it possible to build the type-theoretic equivalent of presheaves, while retaining the good computational properties of our dependent programming languages? We will see that strikingly enough, presheaves can already be presented as computational objects to some extent, except for the annoying fact that they do not obey the right conversion rules! A proper account of type-theoretic presheaves will require a coming-of-age journey through the world of effectful program semantics, using fine and modern tools such as call-by-push-value, dependent parametricity and strict equality. In the end, we will formulate an alternative presentation of presheaves in type theory, but which is still equivalent to its standard categorical counterpart when viewed from the static world of sets. As an application, we will use them to extend dependent type theory with new effective logical principles.
 18/06/2020 SSAFire, a Monadic Gated SSA representation and its optimizations, par Thomas Rubiano
 Thomas Rubiano, INRIA
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24
18/06/2020    10:00 - 11:30
Résumé :
I'll present SSAFire, a variant of the monadic gated Static Single Assignment form, where programs are represented by dependency graphs, rather than control-flow graphs. Its referential transparency makes it useful to implement several global program optimizations as simple graph transformations that can be justified using symbolic and local reasoning.
 11/06/2020 Exploiting Pointer Analysis in Memory Models for Deductive Verification, par Mihaela Sighireanu
 Mihaela Sighireanu, University Paris Diderot, IRIF
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
11/06/2020    14:00 - 15:00
Résumé :
Cooperation between verification methods is crucial to tackle the challenging problem of software verification. I'll present such a collaboration involving static analyzers doing pointer analysis and a deductive verification method based on first order logic. The idea is to exploit the result of pointer analysis in order to provide a memory model to the deductive verification that captures precisely the disjointedness of regions in the program memory. The accuracy obtained in the memory model is essential for shortening aliasing annotations and improve the results of automated solvers. This cooperation has been implemented inside the Frama-C platform.
 08/06/2020 Generating Referring Expressions from RDF Knowledge Graphs for Data Linking , par Armita Khajeh-Nassiri
 Armita Khajeh-Nassiri
Virtuel sur Jitsi: https://jitsi.lipn.univ-paris13.fr/RDFKGforDataLinking
08/06/2020    15:00 - 16:00
Résumé :
In a knowledge graph, a referring [removed]RE) is a logical formula that can uniquely identify an entity. We propose a novel approach for discovering REs that are valid within a class of a knowledge graph. There can potentially exist many REs for each entity, hence we have focused on those descriptions that are 1) minimal 2) diverse and that 3) can not be found by instantiating the keys. As an application, we study the data linking problem that, given two knowledge graphs G1 and G2, finds the possible links between the entities of G1 and G2. We show that REs can drastically improve the quality of data linking. Rejoindre la réunion?: https://jitsi.lipn.univ-paris13.fr/RDFKGforDataLinking
 04/06/2020 Logic Beyond Formulas: A Proof System on Graphs, par Matteo Acclavio
 Matteo Acclavio, SaToSS, Université du Luxembourg
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 638888)
04/06/2020    10:00 - 11:30
Résumé :
In proof theory, proof systems usually operate on formulas, that is, objects characterized by an underlying tree structure. The aim of this talk is to define a proof system operating on general (undirected) graphs instead of formulas. We start from the correspondence between formulas and cographs, i.e. graphs containing no chordless paths of length 3. As a consequence of considering general graphs, we can no longer use the standard proof theoretical methods relying on the tree structure of formulas: for instance, we are not able to identify the main connective of a formula. Thanks to graphs modular decomposition and some techniques from deep inference, we are able to define a proof system with admissible cut and which is a conservative extension of MLL with mix. This talk is based on a joint work with Ross Horne and Lutz Strassburger.
 28/05/2020 A cellular Howe theorem, par Tom Hirschowitz
 Tom Hirschowitz, CNRS & Université Savoie Mont Blanc
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 638888)
28/05/2020    11:00 - 12:30
Résumé :
We introduce a categorical framework for operational semantics, in which we define substitution-closed bisimilarity, an abstract analogue of the open extension of Abramsky's applicative bisimilarity. We furthermore prove a congruence theorem for substitution-closed bisimilarity, following Howe's method. We finally demonstrate that the framework covers the call-by-name and call-by-value variants of lambda-calculus in big-step style. As an intermediate result, we generalise the standard framework of Fiore et al. for syntax with variable binding to the skew-monoidal case. This is joint work with Peio Borthelle and Ambroise Lafont.
 19/05/2020 Focusing on lambda-calculus equivalence, par Gabriel Scherer
 Gabriel Scherer, INRIA
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 638888)
19/05/2020    15:30 - 17:00
Résumé :
In this overview talk we will show how the logical technique of focusing can be applied to better understand program equivalence in the simply-typed lambda-calculus with datatypes (in particular sums and the empty type). The talk will not assume familiarity with focusing, and introduce it in the context of propositional intuitionistic logic. We will then present a focused presentation of the (normal forms of the) lambda-calculus. If time allow, we will then introduce the "saturated" normal forms, a stronger restriction that we used in https://arxiv.org/abs/1610.01213 (2017) to decide equivalence of simply-typed lambda-terms with sums and the empty type.
 07/05/2020 Implicit automata in typed lambda-calculi, par Nguyen Lê Thành Dung
 Nguyen Lê Thành Dung, LIPN, Université Sorbonne Paris Nord
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 638888)
07/05/2020    10:00 - 11:30
Résumé :
We show that various classes of languages and functions from automata theory can be equivalently defined using lambda-calculi with substructural types. For instance, we characterize regular string-to-string functions with affine types, and star-free languages with non-commutative types. These results have few direct precedents, but they are analogous to the field of implicit computational complexity, except with automata instead of complexity classes. Our starting point is the little-known fact that the predicates definable over Church-encoded strings in the simply typed lambda-calculus are exactly the regular languages (Hillebrand & Kanellakis, LICS'96). More recently, similar ideas have played a prominent role in higher-order model checking. This is joint work with Pierre Pradic (University of Oxford).
 30/04/2020 Taylor Subsumes Scott, Berry, Kahn and Plotkin, par Davide Barbarossa
 Davide Barbarossa, LIPN
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 638888)
30/04/2020    10:00 - 11:30
Résumé :
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential lambda-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in lambda-calculus that are usually demonstrated by exploiting Scott's continuity, Berry's stability or Kahn and Plotkin's sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
 23/04/2020 Méthodes primal-dual avec la programmation linéaire des configurations, par Nguyen Kim Thang
 Nguyen Kim Thang, Université d'Evry
Salle B107, bâtiment B, Université de Villetaneuse
23/04/2020    10:30 - 11:30
Résumé :
Primal-duale est une méthode élégante et puissante en optimisation et en algorithmique. La méthode consiste à établir de manière interactive des solutions primals et duales, puis un algorithme, ainsi que son analyse, sont guidés naturellement par l'interaction primal-duale. Dans cet exposé, je vais présenter les approches primal-dual comme techniques unifiées afin d'étudier et de développer les algorithmes les domaines de la théorie des jeux algorithmiques et de l'algorithmique en ligne.
 23/04/2020 The Complexity of Interaction Abstract Machines, par Gabriele Vanoni
 Gabriele Vanoni, Università di Bologna
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 638888)
23/04/2020    10:00 - 11:30
Résumé :
Geometry of Interaction (GOI) is a semantic framework describing the dynamics of cut-elimination in the Multiplicative Exponential fragment of Linear Logic (MELL). It has been formulated in many ways, from operator algebras to traced symmetrical monoidal categories. Remarkably, some of these formulations, in particular Context Semantics by Gonthier et al. led to the introduction of compilation techniques (Mackie '95) and abstract machines for higher-order functional languages (Danos and Regnier '99). However, these machines were always based on a proof-net representation of programs, via the so-called Girard translation. We introduce an abstract machine in the spirit of GOI based directly on the ?-calculus, without any explicit use of proof-nets. We prove soundness and adequacy, and we derive in our framework an optimization already presented by Danos and Regnier. We complete our study with a complexity analysis of those machines.
 16/04/2020 Décomposition et recherche Monte Carlo en General Game Playing, par Nicolas Jouandeau
 Nicolas Jouandeau, Université Paris 8
Salle B107, bâtiment B, Université de Villetaneuse
16/04/2020    12:15 - 13:45
Résumé :
Les jeux permettent de définir des problèmes non triviaux dans un cadre fini et maîtrisé, et offrent de fait un cadre intéressant pour létude des algorithmes de décision. Pour réduire l'influence de connaissances expertes spécifiques à un jeu et stimuler une analyse logique des problèmes, le General Game Playing (GGP) propose de jouer à des jeux inconnus en partant uniquement de la description logique de leurs règles. Dans ce contexte, nous proposons deux méthodes générales de décomposition des jeux décrits en Game Description Language (GDL), l'une sappuyant sur une analyse logique des règles et l'autre sur une analyse statistique dinformations collectées pendant des simulations. Enfin nous présentons une variation de la méthode Monte Carlo Tree Search exploitant ces décompositions dans un joueur GGP et permettant de résoudre simplement certains jeux.
 16/04/2020 Automatic Differentiation in PCF, par Damiano Mazza
 Damiano Mazza, LIPN, CNRS & Université Paris 13
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (access code: 638888)
16/04/2020    10:00 - 11:00
Résumé :
Automatic differentiation (AD) is the science of efficiently computing the derivative (or gradient, or Jacobian) of functions specified by computer programs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for training deep neural networks. Albeit AD techniques traditionally focus on a restricted class of programs, namely first-order straight-line programs, the rise of so-called differentiable programming in recent years has called for the need of applying AD to complex code, containing all sorts of control flow operators and higher-order combinators. In this talk, I will discuss the extension of AD algorithms to PCF, a(n idealized) purely functional programming language. We will first consider the simply-typed lambda-calculus, showing in particular how linear negation is related to reverse mode AD (aka backpropagation), and then see how the extra features of PCF, namely full recursion and conditionals, may be dealt with, stressing the difficulties posed by the latter. [Joint work with Aloïs Brunel (Deepomatic) and Michele Pagani (IRIF, Université de Paris)]
 26/03/2020 Multi-period Hub Location Problem with Serial Demands: A Case Study of Humanitarian Aids Distribution in Lebanon, par Shahin Gelareh
 Shahin Gelareh, Université dArtois
Salle B107, bâtiment B, Université de Villetaneuse
26/03/2020    10:30 - 11:30
Résumé :
We address the problem of humanitarian aids distribution across refugee camps in war-ridden areas from a network design perspective. We show that the problem can be modeled as a variant of multi-period hub location problem with a particular demand pattern resulted by the user's behavior. The problem has been motivated by a case study of Lebanese experience in Syrian war refugee accommodation. We elaborate on the complexity and real-life constraints and, propose a compact formulation of a mathematical model of the problem. We then show that modeling the problem using a Benders paradigm drives O(n^3) variables of the original compact model unnecessary in addition to the constraints that are being projected out in a typical Benders decomposition. Additionally, we identify several classes of valid inequalities together with efficient separation procedures leading to a cut-and-Benders approach. Our extensive computational experiments on the case study with real data as well as randomly generated instances proves the performance of proposed solution methods.
 19/03/2020 REASONING ABOUT DYNAMIC NETWORKS OF INFINITE-STATE PROCESSES , par Mihaela Sighireanu
 Mihaela Sighireanu , University Paris Diderot, IRIF
Salle A303, Institut Galilée, Université Sorbonne Paris Nord
19/03/2020    10:00 - 11:00
Résumé :
We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks. They can be seen as Petri nets where tokens (representing occurrences of processes) are colored by values over some potentially infinite data domain such as integers, reals, etc. Furthermore, we define a logic, called CML (colored markings logic), for the description of CPN configurations. CML is a first-order logic over tokens allowing to reason about their locations and their colors. Both CPNs and CML are parametrized by a color logic allowing to express constraints on the colors (data) associated with tokens. We investigate the decidability of the satisfiability problem of CML and its applications in the verification of CPNs. We identify a fragment of CML for which the satisfiability problem is decidable (whenever it is the case for the underlying color logic), and which is closed under the computations of post and pre images for CPNs. These results can be used for several kinds of analysis such as invariance checking, pre-post condition reasoning, and bounded reachability analysis.
 16/03/2020 What (many kinds of) graphs can contribute to explainable machine learning, par Tiphaine Viard
 Tiphaine Viard, LIPN
Salle B107, bâtiment B, Université de Villetaneuse
16/03/2020    12:15 - 13:45
Résumé :
AI and machine learning are commonly described as "black boxes" that are efficient, but opaque. While complete opacity would be an exaggeration, it is true that many methods for explainability rely on forms of retro-engineering: we try to infer the model from its (partial, intermediary, final) results. These methods are typically based on large-scale, efficient matrix manipulation. Graphs and their extensions have shown to be visualisable and interpretable, even at large scales. In their classical formulation, they are also very similar to matrices, but also versatile: they can be directed, weighted, multilayered, temporal, etc. Each of those extensions giving rise to interesting algorithmic and data-driven questions. To date, few machine learning methods, harness the expressive power of graphs, in part due to the complexities of graph algorithms, typically having polynomial running times, which is incompatible with the scale of data at hand. However, the situation has changed: (i) the impact of AI on society makes it no longer acceptable to only favour efficiency despite explainability, and (ii) recent advances in algorithmic methods on graphs demonstrates that due to the nature of real-world graphs, even some NP-hard problems become tractable. The aim of this talk is to explore this avenue of research. We will discuss the state-of-the art as well as some past results in real-world (temporal) graph modeling and in explainability, and will then discuss some recent results on pattern mining on temporal graphs.
 10/02/2020 Attention is all I need, par José Angel Gonzalez-Barba
 José Angel Gonzalez-Barba, Universidad Politécnica de Valencia
Salle B107, bâtiment B, Université de Villetaneuse
10/02/2020    12:30 - 13:30
Document attaché
Résumé :
The use of attention mechanisms has been widespreaded along all the natural language processing tasks. These kind of mechanisms have increased the capacity of Deep Learning models allowing them to focus explicitly on the most discriminant relationships and properties for a given task. Recently, the Transformer model have replaced Convolutional and Recurrent neural networks in many NLP tasks, mainly due to its capability of modeling sequences, avoiding the sequential processing by using only attention mechanisms. In this talk I will speak about the application of the Transformer encoders to text classification in social media (Sentiment Analysis and Irony Detection in Twitter) and its application in a novel framework for extractive summarization. About the author: José Angel just finished his PhD and he is going to start a PostDoc in the group of Yoshua Bengio at the University of Montreal. His works on Spanish NLP have been very promising and he developed some state-of-the-art systems for sentiment analysis and summarization.
 30/01/2020 On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem, par Raphaëlle Crubillé
 Raphaëlle Crubillé, IMDEA
Salle B107, bâtiment B, Université de Villetaneuse
30/01/2020    10:15 - 12:00
Résumé :
I will present a joint work with Barthe, Dal Lago and Gavazzo. Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used exten- sively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of log- ical relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally ex- pressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we introduce a generalization of the concept of a logical relation, which we dub open logi- cal relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed ?-calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of con- tinuous or differentiable functions. We first prove a containment theorem stating that for any such a collection of functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open logical relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Fi- nally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open logical relations.
 20/12/2019 Parametric schedulability analysis of a launcher flight control system under reactivity constraints, par Jawher Jerray
 Jawher Jerray, LIPN
Salle B107, bâtiment B, Université de Villetaneuse
20/12/2019    15:00 - 15:30
Résumé :
The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this work, we present an approach on the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool in an optimal way. We first describe the problematic of the scheduling of a launcher flight control, then we show how this problematic can be formalized with parametric stopwatch automata; we then present the results computed by IMITATOR. We compare the results to the ones obtained by other tools classically used in scheduling.
 20/12/2019 Concurrent Algorithms and Data Structures for Model Checking, par Jaco van de Pol
 Jaco van de Pol, Aarhus University
Salle B107, bâtiment B, Université de Villetaneuse
20/12/2019    14:00 - 15:00
Résumé :
Model checking is a successful method for checking properties on the state space of concurrent, reactive systems. Since it is based on exhaustive search, scaling the method to industrial systems has been a challenge since its conception. Research has focused on clever data structures and algorithms, to reduce the size of the state space or its representation; smart search heuristics, to reveal potential bugs and counterexamples early; and high-performance computing, to deploy the brute force processing power of clusters of compute-servers. The main challenge is to combine a brute force approach with clever algorithms: brute force alone (when implemented carefully) can bring a linear speedup in the number of processors. This is great, since it reduces model-checking times from days to minutes. On the other hand, proper algorithms and data structures can lead to exponential gains. Therefore, the parallelization bonus is only real if we manage to speedup clever algorithms. There are some obstacles: many linear-time graph algorithms depend on a depth-first exploration order, which is hard to parallelize. Examples include the detection of strongly connected components (SCC), and the nested depth-first-search (NDFS) algorithm. Both are used in model checking LTL properties. Symbolic representations, like binary decision diagrams (BDDs), reduce model checking to "pointer-chasing", leading to irregular memory-access patterns. This poses severe challenges on achieving actual speedup in (clusters of) modern multi-core computer architectures. This talk will present some of the solutions found over the last 10 years, leading to the high-performance model checker LTSmin. These include parallel NDFS (based on the PhD thesis of Alfons Laarman), the parallel detection of SCCs with concurrent Union-Find (based on the PhD thesis of Vincent Bloemen), and concurrent BDDs and other decision diagrams (based on the PhD thesis of Tom van Dijk). This functionality is provided in a specification-language agnostic manner, while exploiting the locality typical for a-synchronous distributed systems (based on the PhD thesis of Jeroen Meijer). Finally, I will sketch a perspective on moving forward from high-performance model checking to high-performance synthesis algorithms. Examples include parameter synthesis for stochastic and timed systems, and strategy synthesis for (stochastic and timed) games. The focus of the talk will be on a parallel algorithm for SCC decomposition
 17/12/2019 Parallel verification of concurrent systems using the Symbolic Observation Graph, par Hiba OUNI
 Hiba OUNI, LIPN
Salle A303
17/12/2019    12:30 - 13:30
Résumé :
Model checking is one of the major techniques used in formal verification. This technique takes a model of a system in question and decides whether it satisfies a given property or not. It is based on an exhaustive exploration of the state space of the system to be verified. Thus, the Model checking technique suffers from the state space explosion problem: it can happen that the verification process stops because of lack of time or space. One of the proposed solutions to tackle this problem is to parallelize the verification process. The use of distributed processing increases the speedup and scalability of model checking by exploiting the cumulative computational power and memory of a cluster of computers. Such approaches have been studied in various contexts leading to different proposed solutions for both symbolic and explicit model checking. In this talk, we shall present new model checking algorithms built on a parallel construction of the Symbolic Observation Graph: an abstraction of the state space graph that preserves Linear Temporal Logic (LTL). We implemented the proposed model checking algorithm within a C++ prototype and compared our preliminary results with the state of the art model checkers.
 14/11/2019 Formal Specification and Verification of Interactive Multimedia Scores, par Jaime Arias
 Jaime Arias, LIPN
Salle A303
14/11/2019    13:00 - 14:00
Résumé :
Interactive Scores (IS) is a formalism for composing and performing interactive multimedia scores with several applications in video games, live performance installations, and virtual museums. In this model, the composer defines the temporal organization of the score by asserting temporal relations (TRs) between temporal objects (TOs). At execution time, the performer may modify the start/stop times of the TOs by triggering interaction points while the system guarantees that all the TRs are satisfied. Implementations of IS and formal models of their behavior have already been proposed, but these do not provide usable means to reason about their properties. In this talk we presente a Timed Automata model that fully captures the temporal structure of IS during both composition and execution, and that makes it possible to reason about the written scores.
 07/11/2019 Journee CoGITARe, par Divers
 Salle B107, bâtiment B, Université de Villetaneuse 07/11/2019    10:00 - 17:00 Résumé : Quatre exposés autour de l'inférence de types pour divers systèmes avec intersection et union. Exposants : Stephen Dolan, Giuseppe Castagna, Claude Stolze et Flavien Breuvart programme : https://lipn.univ-paris13.fr/~breuvart/CoGITARe/journee_inferencing_subtypes.php?lang=uk
 24/10/2019 Relative monads for relational reasoning, par Kenji Maillard
 Kenji Maillard, Inria Paris
Salle B107, bâtiment B, Université de Villetaneuse
24/10/2019    10:15 - 12:00
Résumé :
Relational verification is concerned with the problem of proving specifications relating either two runs of a single program, such as non-interference, or two different programs, for instance simulations or equivalences. Starting with Benton's Relational Hoare Logic for imperative programs, many varieties of relational program logics have been designed for specific classes of relational properties and effects. Focusing on the setting of monadic computations, we want to design a generic framework for relational program logics. In our quest to understand the federating principles underlying relational reasoning, we explain how basic core properties of relational program logics are suitably captured by relative monads, a generalization of monads that need not to be an endofunctor. Working "over the product", these relative monads establish a bridge between two computational monads, employed to encapsulate their relational specifications.
 17/10/2019 Explicative Data Analytics, par Martin Atzmüller
 Martin Atzmüller, Tilburg University
Salle B107, bâtiment B, Université de Villetaneuse
17/10/2019    14:00 - 16:00
Résumé :
Modeling and mining multi-modal and heterogeneous data is important in the context of analyzing knowledge and information processes in complex environments, e.g. for mining high dimensional and heterogeneous (sensor) data, the analysis of exceptional patterns, and complex network structures. For making sense of the data, explicative data analytics focuses on interpretable, transparent and explainable approaches, which is relevant for very many applications for analyzing data in science and industry. The talk presents according approaches for explicative data analytics incorporating methods from data science, machine learning, and human computing, exemplified by multi-modal sensor data analysis, pattern mining and graph analytics.
 03/10/2019 Optimal Transport for Machine Learning, par Bernard Kamsu-Foguem
 Bernard Kamsu-Foguem, ENIT, Tarbes
Salle B107, bâtiment B, Université de Villetaneuse
03/10/2019    12:15 - 13:45
Résumé :
Optimal transport defines a set of geometric tools with interesting properties (comparison and morphology of probability measurements) that make it particularly suitable for solving large scale artificial learning problems. Since probability distributions are omnipresent in Machine Learning (ML), whether theoretical or empirical, optimal transport can be useful in order to measure their separation or, even better, to be able to transform them at a lower cost. We will investigate techniques based on optimal transport in certain practical and theoretical contexts (text classification, multi-label classification and domain adaptation), to contribute to solving the associated Machine Learning (ML) problems.
 30/09/2019 Détection de la radicalisation sur les réseaux sociaux, par Frédérique Segond
 Frédérique Segond, Inalco
Salle C316
30/09/2019    12:30 - 13:30
Résumé :
Dans ce séminaire je présenterai le travail effectué dans le cadre du projet européen Saffron pour détecter la radicalisation sur les réseaux sociaux. Après avoir présenté la problématique et lapproche multidisciplinaire adoptée, je me focaliserai sur la description des modules danalyse sémantique, en particulier sur le module dextraction dévénements. Jillustrerai mon propos avec les difficultés rencontrées et parlerai de la difficulté dévaluer un tel travail. Je conclurai en présentant les perspectives actuelles de ce travail par rapport à des projets en cours et à la plateforme MediaCentric développée chez Bertin IT.
 25/09/2019 Brzozowski and Antimirov reordering derivatives, par Tarmo Uustalu
 Tarmo Uustalu, Reykjavik / Tallinn
Salle B107, bâtiment B, Université de Villetaneuse
25/09/2019    14:00 - 15:00
Résumé :
The Brzozowski and Antimirov derivatives are effective operations on regular expressions that calculate the (semantic) derivatives of a regular language. They yield constructions of finite deterministic and nondeterministic automata. In this talk, I show how these operations on regular expressions admit natural generalizations for trace closures of regular languages, which are languages obtained from a regular language by allowing some pairs of letters to commute. The automata from the Brzozowski and Antimirov reordering derivatives are generally not finite. But if the regular expression is star-connected or, more generally, if its language has uniform rank, they are. This is joint work with Hendrik Maarand. I will also give a short introduction to what we do in my groups in Tallinn and Reykjavik.
 24/09/2019 Quelques problèmes d'optimisation dans les réseaux, par Cedric Bentz
 Cedric Bentz, CNAM
Salle B107, bâtiment B, Université de Villetaneuse
24/09/2019    12:30 - 13:30
Résumé :
J'évoquerai dans cet exposé quelques problèmes d'optimisation dans les réseaux auxquels je me suis intéressé, parfois en collaboration avec d'autres chercheurs, depuis quelques années. Dans certaines des variantes étudiées, les réseaux considérés peuvent être sujets aux pannes, ce qui peut nécessiter d'en tenir compte lors de la conception de tels réseaux. La première famille de problèmes étudiés tourne autour de généralisations du problème de multicoupe, prenant notamment en compte le fait que le bon fonctionnement d'un réseau peut être mis en cause même si seul un certain nombre des communications à assurer sont affectées, pour lesquelles des résultats de complexité paramétrée ont été récemment obtenus dans différents cas particuliers. La seconde famille tourne autour de problèmes de d-bloqueurs dans les graphes, dans lesquels on s'intéresse au nombre minimum de noeuds (sommets) ou de liens (arêtes) qui doivent tomber en panne pour que, intuitivement, le réseau descende en-dessous d'un certain seuil de fonctionnement. Plusieurs résultats de complexité notables ont ainsi été obtenus pour cette catégorie de problèmes, dont on ne sait souvent même pas déterminer facilement s'ils sont dans NP ou non. Enfin, la troisième et dernière famille tourne autour de problèmes d'arbres et de réseaux de Steiner, en présence de capacités, et dans certains cas de pannes. Concernant le problème d'arbre de Steiner avec capacités sur les arcs mais sans pannes, les résultats de complexité qui ont été obtenus permettent d'obtenir une caractérisation complète de la complexité de ce problème vis-à-vis de plusieurs paramètres. Concernant le problème de conception de réseaux de Steiner avec capacités et pannes, plusieurs formulations le modélisant, dont une formulation biniveau, ont été obtenues et comparées entre elles, de façon théorique comme expérimentale, et quelques inégalités permettant de les renforcer ont également été testées. Ces formulations peuvent toutes être adaptées au cas où l'on ajoute la possibilité de protéger un certain nombre de liens du réseau, mais un fait notable et pas nécessairement intuitif est que les relations entre les formulations diffèrent alors du cas précédent.
 19/09/2019 Unifying abstract and linear rewriting. , par Maxime
 Maxime, Lucas
Salle B107, bâtiment B, Université de Villetaneuse
19/09/2019    10:00 - 11:30
Résumé :
As opposed to abstract rewriting (where one studies a set of term up to some rewrite rules), linear rewriting consists in studying linear combinations of terms, up to some rewrite rules. However the naive definitions of termination does not work in this case. The usual solution consists in only considering well-formed rewriting steps. This however is not very satisfactory because usual rewriting lemmas cannot be applied directly to the linear case and have to be proven again. In this talk we present a formalism unifying the abstract and linear cases, based on the notion of reduction strategy. In this setting, we recover an analogue of Newman's Lemma, while weakening the termination hypothesis.
 17/09/2019 Algorithmes auto-stabilisants, par Lélia Blin
 Lélia Blin, Sorbonne Université LIP6
Salle B107, bâtiment B, Université de Villetaneuse
17/09/2019    12:30 - 13:30
Résumé :
Dans le contexte des réseaux à grande échelle, la prise en compte des pannes est une nécessité. L'auto-stabilisation est une approche algorithmique de la tolérance aux pannes dans les systèmes distribués dont le but est de gérer la corruption de la mémoire des processeurs dues à des pannes transitoires. Plusieurs paramètres caractérisent l'efficacité d'un algorithme auto-stabilisant, dont en particulier (1) le temps pris par le système pour retourner dans une configuration légale suite à une corruption arbitraire de la mémoire de ses processeurs, et (2) l'espace mémoire utilisé par les processeurs pour exécuter l'algorithme. La minimisation de l'espace mémoire est motivée pas de nombreux aspects : existence de réseaux (tels que les réseaux de capteurs) offrant des espaces mémoires limités, la minimisation des échanges de données entre processeurs voisins, la limitation du stockage d'information afin de pouvoir utiliser des techniques de redondance, etc. Ce séminaire présentera l'auto-stabilisation au travers deux grands problèmes classiques : la construction d'arbres couvrants, notamment d'arbres couvrants de poids minimum, et l'election d'un leader. Il présentera en particulier les liens entre auto-stabilisation et les techniques de décision distribuée, incluant le calcul de bornes inférieures sur l'espace mémoire nécessaire à la résolution par des algorithmes auto-stabilisants des problèmes susmentionnés.
 03/07/2019 The Robust Capacitated Facility Location Problem, par Marco Caserta
 Marco Caserta, IU Business School
Salle B107, bâtiment B, Université de Villetaneuse
03/07/2019    14:00 - 15:00
Résumé :
We present robust formulations for the capacitated facility location problems under demand uncertainty, both for the single-source and the multi-source variants. Robustness is defined over different uncertainty sets, i.e., the box, ellipsoidal, and polyhedral uncertainty sets. For each of these variants, we define the robust counterpart and we compare the results obtained through an extensive computational study. We test the effect of using different support sets and analyze the performance of each robust variant using scenario curves and price of robustness, among other measures.
 02/07/2019 Aspects combinatoires du problème de l'UCP, par Pierre Fouilhoux
 Pierre Fouilhoux, Lip6 - Paris 6 - Sorbonne Université
Salle B107, bâtiment B, Université de Villetaneuse
02/07/2019    12:30 - 13:30
Résumé :
Le problème classique appelé Unit Commitment Problem (UCP) est le problème central de planification de production d'électricité. Le problème combinatoire au coeur du problème de l'UCP est appéle le Min-up/min-down UCP (MUCP). Il consiste à déterminer un plan de production sur un horizon de temps discrétisé, pour un ensemble de centrales électriques. A chaque pas de temps, la production totale doit répondre à une demande connue. Chaque unité doit satisfaire des contraintes de temps minimum de fonctionnement et d'arrêt. Elle correspond également à des coûts de production et de mise en marche. Nous étudions comment la complexité du MUCP évolue en fonction du nombre d'unités et de période. Nous montrons en particulier que ce probl&egrav e;me est NP-difficile au sens fort. Nous présentons plusieurs aspects polyédraux d'une formulation PLNE pour le MUCP en nous intéressant à la combinatoire liant la production des unités entre les pas de temps. Pour cette formulation, l'espace des solutions exploré par un algorithme de branchement contient de nombreuses solutions symétriques et sous-symétriques: deux solutions symétriques (resp. sous-symétriques) pouvant être obtenues l'une de l'autre par permutation de ses composantes (resp. d'une partie de ses composantes). Nous proposons deux techniques bien distinctes pour briser ces symétries et accélérer la résolution. La première technique s'appuie sur l'étude du polyèdre des permutations et sur un algorithme, dit de fixing, utilisé à chaque noeud de l'algorithme de branchement. La deuxième technique repose sur des inégalités linéaires et des variables additionnelles. Enfin, nous présentons plusieurs aspects prometteurs sur une nouvelle décomposition de Dantzig-Wolfe qui utilise plusieurs inégalités issues de notre étude polyèdrale. Travaux réalisés avec Pascale Bendotti et Cécile Rottner.
 26/06/2019 La Maison des Maths d'Ispahan, par Amir Hashemi
 Amir Hashemi, Université Technologique d'Ispahan
Salle B107, bâtiment B, Université de Villetaneuse
26/06/2019    14:00 - 15:00
Résumé :
Dans une première partie, je présenterai le système de recherche et enseignement supérieur des universités iraniennes et discuterai de ses performances. Dans une seconde partie, je présenterai les missions et activités des Maison des Mathématiques iraniennes, dont la première a été établie en 1999 à Ispahan. Il s'agit donc d'un exposé non technique, plutôt meta-scientifique. Il sera accompagné de quelques gâteaux iraniens.
 25/06/2019 Optimisation et Bicliques, par Denis Cornaz
 Denis Cornaz, LAMSADE - Paris Dauphine
Salle B107, bâtiment B, Université de Villetaneuse
25/06/2019    12:30 - 13:30
Résumé :
Un sous-graphe partiel, d'un graphe donné, est une biclique, de ce graphe, s'il est biparti complet. D'abord, nous passerons en revue des résultats classiques admettant des preuves élégantes, voir surprenantes, autour de cette notion. Ensuite, nous mènerons une étude structurelle, particulière à cette notion, permettant de mettre en uvre une technique générale d'optimisation (branch-and-cut, -and-price). Nous terminerons par une conjecture récemment démontrée.
 24/06/2019 Identity links in knowledge graphs, par Nathalie Pernelle
 Nathalie Pernelle, LRI, Université Paris Sud
Salle B107, bâtiment B, Université de Villetaneuse
24/06/2019    16:00 - 17:00
Résumé :
As the Web of Data continues to grow, more and more large datasets  covering a wide range of topics and domains  are being added to the Linked Open Data (LOD) Cloud. It is inevitable that different datasets, most of which are developed independently of one another, will come to describe (aspects of) the same thing, but will do so by referring to that thing by different names. Thanks to identity links, datasets that have been constructed independently of one another are still able to make use of each others information. Many data linking approaches have been defined that are rule-based. Some of these approaches exploit ontology axioms such as keys. However, these axioms are rarely specified in the available ontologies. In this seminar, I will present two approaches that aim to discover more or less expressive keys in RDF data. Then, since data linking approaches do not obtain a 100% precision, I will show that some approaches can focus on detecting incorrect sameAs links or detect that they are valid only in a specified semantic context.
 19/06/2019 Data Explainability Through Linguistic Expression of Extracted Knowledge, par Marie-Jeanne Lesot
 Marie-Jeanne Lesot, LIP6
Salle B107, bâtiment B, Université de Villetaneuse
19/06/2019    12:15 - 13:30
Résumé :
The pervasive use of data science techniques extracts regularities from available data for different tasks, such as prediction, characterisation or structuring. A current challenge is to improve the legibility of the obtained results, so as to allow a data expert to understand better the content of the data. One way to address this challenge consists in presenting them in natural language, offering linguistic expressions which may be easier to interpret for the user. The choice of such a result formulation then has an impact on the machine learning techniques to be applied to the data. The talk will illustrate these questions for numerical data as well as for time series, respectively discussing the extraction of gradual itemsets, that linguistically express knowledge about feature covariations, and the extraction of periodicity-related linguistic summaries, using the specific quantifier regularly. In both cases, as well as for enriched contextual variants, the question is to define precisely the associated semantics and to design efficient extraction algorithms. The talk will also discuss the issue of measuring the relevance of the linguistic terms used to express the summaries, both with respect to the data structure, in case of linguistic variables, and with respect to the cognitive interpretation, in case of approximate numerical expressions.
 18/06/2019 Parametric schedulability analysis of a launcher flight control system under reactivity constraints, par Jawher Jerray
 Jawher Jerray, Équipe LoVe, LIPN
Salle A303
18/06/2019    13:00 - 13:30
Résumé :
The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. We present an approach on the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We describe the problematic of the scheduling of a launcher flight control, then we show how this problematic can be formalized with parametric stopwatch automata; we then present the results computed by IMITATOR.
 18/06/2019 Towards parallel verification of concurrent systems using the Symbolic Observation Graph, par Hiba OUNI
 Hiba OUNI, Équipe LoVe, LIPN
A303
18/06/2019    12:30 - 13:00
Résumé :
An efficient way to cope with the combinatorial explosion problem induced by the model checking process is to compute the Symbolic Observation Graph (SOG). Given a stutter-invariant event-based LT L formula ?, involving a subset of actions (called observable actions), the SOG is a condensed representation of the state space graph based on a symbolic encoding of the nodes (sets of states linked with unobservable actions) and an explicit representation of the edges (labelled with observable actions). It has the advantage to be much reduced comparing to the original state space graph while being equivalent with respect to stutter-invariant temporal properties (i.e., the original system satisfies ? if and only if the corresponding SOG satisfies ?). Aiming to go fu rther in the process of tackling the state space explosion problem, we propose in this paper to parallelize the construction of the SOG using a hybrid approach (distributed+shared memory). Doing so, we take advantage of the recent advances in computer hardware, by distributing the construction process over a large number of multi-core processors. We studied the performances of our new approach comparing to both distributed and shared memory approaches on one side, and to the sequential construction on the other side. The obtained results show that the proposed approach offers an interesting alternative allowing to completely exploit the available distributed architecture while offering significant speedup.
 13/06/2019 La logique du signe : Sémiologie structuraliste et typage par biorthogonalité pour l'analyse de corpus., par Juan Luis Gastaldi
 Juan Luis Gastaldi, ETH Zürich, SPHERE Paris Diderot
Salle B107, bâtiment B, Université de Villetaneuse
13/06/2019    10:30 - 12:30
Résumé :
Dans cette conférence, il s'agira de présenter le cadre théorique et conceptuel d'une recherche en cours associant le projet d'une théorie formelle du signe d'inspiration structuraliste à certains principes et ressources de la linguistique de corpus et de la logique linéaire. L'objectif de ce travail interdisciplinaire est d'inférer de façon non supervisée des structures grammaticales ou logiques émergentes pour tout système de signes donné sous la forme d'un corpus d'expressions. L'analyse formelle proposée se base sur une procédure de segmentation stratifiée et de typage par biorthogonalité, capable, en principe, de capturer des structures de tous les niveaux (phonologiques ou graphématiques, morphologiques, syntaxiques et sémantiques). D'un point de vue philosophique, la perspective adoptée implique une manière originale de rapporter la logique au langage et à d'autres systèmes naturels de signes.
 05/06/2019 Alice au pays des frises et des pavages, par François Bergeron
 François Bergeron, UQAM
Salle B107, bâtiment B, Université de Villetaneuse
05/06/2019    14:00 - 15:00
Résumé :
La notion de frise dentiers a été introduite dans les années 1970 par Conway et Coxeter. Une telle frise correspond à un nombre fini de bandes horizontales superposées dentiers positifs (>0), bornées au-dessus et en dessous par des bandes de 1, avec une condition locale liant ces entiers. Plus explicitement on demande que ad-bc=1, pour toute configuration locale de a, b, c, et d en forme de «?diamant?» (a et d se suivent sur une même ligne, avec b et c respectivement juste au-dessus et en dessous). Conway et Coxeter ont souligné que cela force un phénomène de répétition cyclique horizontale; de là le terme de frise. Un autre aspect fascinant est qu il ny a quun nombre fini de telles frises ayant un nombre fixé de lignes, et quelles sont énumérées par les nombres de Catalan. Après un survol de cette notion et de sujets reliés, nous allons en considérer diverses généralisations. En particulier, on établira des liens avec la formule de condensation de Dogdson (lauteur dAlice au pays des merveilles) pour un calcul récursif de déterminants.
 23/05/2019 Towards a Combinatorial Proof Theory, par Ben Ralph
 Ben Ralph, Inria Saclay
Salle B107, bâtiment B, Université de Villetaneuse
23/05/2019    14:00 - 16:00
Résumé :
Combinatorial proofs have been introduced by Hughes to give a syntax-free'' presentations for proofs in classical propositional logic. In a nutshell, a classical combinatorial proof consists of two parts: (i) a linear part, and (ii) a skew fibration. The linear part encodes a proof in multiplicative linear logic (MLL), whose conclusion is given represented in a cograph, while the skew fibration maps this linear cograph to the cograph of the conclusion of the whole proof. For deep inference proofs, this skew fibration corresponds exactly to a contraction-weakening derivation. Applying certain restrictions to these two rules leads to substructural logics and substructural proof theory. These proof theoretic restrictions correspond precisely to set-theoretic and graph-theoretic restrictions on the skew fibration, allowing us to characterise proof systems by their graph homomorphism class.
 23/05/2019 Universal and best approximation through Bayesian ARTMAP, par Lucian SASU
 Lucian SASU, Transilvania University of Brasov (Romenia)
Amphi Ampere
23/05/2019    14:00 - 15:30
Résumé :
Bayesian ARTMAP is an adaptive resonance-theory based model, which was extended to perform regression. The network is shown to have both universal and best approximation properties. The network architecture and learning algorithm are presented, along with sketches of proofs and open questions.
 23/05/2019 Rigid species and normal functors over groupoids , par Zeinab Galal
 Zeinab Galal, IRIF
Salle B107, bâtiment B, Université de Villetaneuse
23/05/2019    10:30 - 12:00
Résumé :
Species of structures were introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics. Species are connected to Girard's normal functor semantics of ?-calculus where terms are interpreted as power series with sets as coefficients. Fiore et al. presented a generalised definition that both encompasses Joyal's species and constitutes a model of differential linear logic (DiLL). For generalised species of structures, types are interpreted as groupoids which provides the connection with combinatorics whereas they are interpeted as sets in Girard's normal functors. To investigate how these models interact, we show that all the interpretations of proofs in DiLL actually live in a smaller fragment of generalised species called rigid species. These species correspond to the concept of free groupoid actions which provides us with a notion of normal functors over groupoids and allows us to bridge the gap between species and normal functors.
 22/05/2019 Theoretical and Applied Research in Machine Learning, par Lucian SASU
 Lucian SASU, Transilvania University of Brasov, Roumanie
Salle B107, bâtiment B, Université de Villetaneuse
22/05/2019    14:00 - 14:45
Résumé :
Some insights and experiences in theoretical and applied research are shared. The two worlds are quite different and complementary. The presentation exposes challenging topics in industry which can be addressed through ML, along with hints for researchers willing to join industrial R&D departments.
 17/04/2019 Résumé de texte translingue par compression, par José Manuel Torres-Moreno
 José Manuel Torres-Moreno, LIA, U.Avignon
Salle B107, bâtiment B, Université de Villetaneuse
17/04/2019    14:30 - 15:30
Résumé :
Le Résumé Translingue de Textes (RTT) vise à générer un résumé dans une langue autre que le document source. Plus précisément, le RTT consiste à analyser un document dans une langue source pour en extraire sa signification, puis à générer un résumé court, informatif et correct dans une langue cible. Ce processus peut être divisé en deux processus principaux : le résumé et la traduction. Processus souvent antagonistes. Nous avons développé un cadré expérimentale pour générer des résumés translingues de documents en anglais, français, portugais, espagnol vers {anglais, français}. Nous avons utilisé des applications du TALN (résumé par extraction, similarité de phrases, compression de phrases et fusion multi-phrases) et des approches neuronales pour construire nos modèles de RTT. Cette présentation sera ciblée sur les techniques et les résultats obtenus lors de nos expériences.
 16/04/2019 Run-time Monitoring Approach for Hardware Trojans Dectection, par Maha Naceur
 Maha Naceur, Université Paris 13
Salle A303, bâtiment A, Université de Villetaneuse
16/04/2019    12:30 - 13:30
Résumé :
Todays integrated circuits are vulnerable to malicious activities and alterations such as Hardware Trojan Horses (HTH), which can alter the functioning of the circuit, either during design or fabrication. Run-time monitoring is a predominantly used technique to validate a design in industry. Formal veri?cation overcomes the weakness of exhaustive simulation by applying mathematical methodologies to prove design correctness in an automated way. The design is analysed only against their functional characteristics, and their parametric behavior are do not considered in order to analyze the effects of HTHs. In this work, we present a new approach which focuses upon a combined technique that integrates the best characteristics of both run-time monitoring and formal veri?cation methods to provide an effective design validation tool which uses assertions to automatically generate synthesizable monitors capable for detecting hardware trojan horses at runtime
 04/04/2019 Apprentissage automatique à partir de données complexes et dynamiques: Application aux données textuelles, par Parisa RASTIN
 Parisa RASTIN, LIPN
Salle B107, bâtiment B, Université de Villetaneuse
04/04/2019    13:30 - 14:30
Résumé :
Les données actuelles sont de plus en plus variées et complexes et il est en général nécessaire dadapter les algorithmes danalyse à chaque type de description des données. Les algorithmes dapprentissage devraient cependant pouvoir être fonctionnels quel que soit le type des données et la métrique choisie. Nous présentons dans cet exposé un algorithme de clustering relationnel basée sur le système de Coordonnées Barycentriques pour homogénéiser la représentation des objets et des prototypes et traiter de grands ensembles de données complexes. Dans le système de Coordonnées Barycentriques, lespace de représentation est défini par un ensemble unique de points de support choisis parmi les objets de la base d'apprentissage. La définition dun prototype correspond au calcul dun objet dans lespace barycentrique. À partir de ces approches, nous proposons un algorithme d'apprentissage basé sur un réseau de neurones artificiel défini dans l'espace barycentrique, adapté aux flux de données textuelles et permettant un suivit dynamique de l'évolution des données au cours du temps. Nous présenterons une applications concrètes sur lextraction de domaines dintérêt extraits dURLS à partir de trace de navigation en ligne.
 02/04/2019 Continuous models of computation: computability, complexity,, par Amaury Pouly
 Amaury Pouly, IRIF
Amphy Ampère
02/04/2019    14:00 - 15:30
Résumé :
Et un cours abstract si nécessaire: In 1941, Claude Shannon introduced a continuous-time analog model of computation, namely the General Purpose Analog Computer (GPAC), [which can be implemented in practice through the use of analog electronics or mechanical devices]. In this talk, we review some recents results on the link between the GPAC and Turing machines. We will also see a surprising result on universal polynomial differential equations. Finally, I will also mention some recent application of this work to show that chemical reaction networks are strongly Turing complete with the differential semantics.
 02/04/2019 Fault-tolerant matrix factorisation: a formal model and proof, par Daniel Torres
 Daniel Torres, LIPN, Équipe LoVe
Salle A303, bâtiment A, Université de Villetaneuse
02/04/2019    12:30 - 13:30
Résumé :
As the size of high performance systems grows, tolerating failures has become a major issue in parallel computing. In this paper, we present a Coloured Petri Net model for a fault tolerant matrix factorisation algorithm. On the model, we prove resiliency properties and completion of the algorithm in presence of failures whatever the size of the input. This illustrates how formal modelling and verification techniques can help designing proofs on distributed algorithms.
 27/03/2019 Journée IA du LIPN
Amphi Euler
27/03/2019    09:00 - 18:00
Résumé :
Cette journée est organisée par le Laboratoire dInformatique de Paris Nord LIPN a pour but de présenter des travaux en intelligence artificielle, soit réalisés par des chercheurs du LIPN soit réalisés par des chercheurs extérieurs aussi bien académiques quindustriels. Cette journée aura lieu dans lamphithéâtre Euler de linstitut Galilée. Linscription est gratuite mais obligatoire.
 19/03/2019 The size-change principle for mixed induction and coinduction, par Pierre Hyvernat
 Pierre Hyvernat, Lama (Université de Savoie, Chambéry)
C 304
19/03/2019    14:00 - 16:00
Résumé :
The Size-Change Principle (SCP) is a simple algorithm giving a partial termination test for recursive definitions. If the language is lazy, it also gives (by duality) a partial productivity test for recursive functions involving coinductive types. This is what is used in Agda. Unfortunately, when inductive and coinductive types are nested, this is unsound: there are "well typed" and terminating recursive definitions producing terms in empty types. Such definitions make Agda inconsistant. Using ideas from L. Santocanale about circular proof and parity games, I'll show how the SCP can be used to check "totality" of recursive definitions. Besides the SCP, the main ingredient is a more informative of call-graph, and I'll sketch the proof of correctness by defining their semantics using power domains.
 19/03/2019 Modeling, Analysis and Design of Critical Systems, par Prof. Nejib Ben Hadj-Alouane
 Prof. Nejib Ben Hadj-Alouane, National Engineering School of Tunis (ENIT) - OASIS Lab (Optimization, Analysis of Industrial Systems and Services)
Salle A303, bâtiment A, Université de Villetaneuse
19/03/2019    12:30 - 13:30
Document attaché
Résumé :
Our work on critical systems targets a number of problem areas and applications, all requiring the development of models for analysis and verification, and tools for decision making. This talk focuses on four different problem areas, each requiring a different modeling framework and solution approach. We begin by exposing our new Petri nets modeling framework, Extended Timed Petri Nets (ETPN), useful in modeling a special class of hybrid systems, with a weak continuous component and a strong discrete one, encountered when dealing with modern man-made, embedded and real-time systems. We discuss a supervisory control problem based on this framework, along with other related issues dealing with model transformation and complexity. Our second problem addresses operating high-demand and high-performance virtualized data centers (DCs). We focus on the development of tools, based on operations research models and techniques, for the management of theses DCs, while striving to improve user applications performance and productivity. We focus on the problem of virtual machines (VMs) placement in geographically distributed data centers. We consider communicating VMs assigned to data centers that are connected via a backbone network. We aim to plan and optimize the placement of VMs in data centers so as to minimize the IP-traffic within the backbone network along with user service interruption. Our third problem deals with security and in computer systems, services and protocols. We use the property of opacity to capture secrecy-related problems. We focus on the development of an on-line method for the efficient verification of opacity in models based on automata. We also extend opacity with the introduction of a quantification measure. Our fourth problem deals with sensor networks and their use in precision agriculture. We show that the development of application-oriented infrastructure management techniques, such a routing protocols, is important for modern Fog/IoT networks. Throughout our talk we discuss several research perspectives and applications linked to modern technologies, such as IoT, Web Services and Cloud/Fog computing.
 19/03/2019 Inequalities between plethysm coefficients and Kronecker coefficients via geometric complexity theory, par Christian Ikenmeyer
 Christian Ikenmeyer
Salle B107, bâtiment B, Université de Villetaneuse
19/03/2019    10:30 - 12:00
Résumé :
Research on Kronecker coefficients and plethysms gained significant momentum when the topics were connected to geometric complexity theory, an approach towards computational complexity lower bounds via algebraic geometry and representation theory. Both types of coefficients appear independently in R. Stanley's list of "Positivity problems and conjectures in algebraic combinatorics". This talk is about a result that was obtained with geometric complexity theory as motivation, namely an inequality between rectangular Kronecker coefficients and plethysm coefficients. The proof interestingly uses insights from algebraic complexity theory. As far as we are aware, algebraic complexity theory has never been used before to prove an inequality between representation theoretic multiplicities. This is joint work with Greta Panova (Rectangular Kronecker coefficients and plethysms in geometric complexity theory, Adv Math 2017).
 11/03/2019 Structure Prediction Energy Network (SPEN) using Dual Decomposition on Dependency Parsing, par Xudong ZHANG
 Xudong ZHANG, LIPN - RCLN
Salle B107, bâtiment B, Université de Villetaneuse
11/03/2019    14:00 - 15:00
Résumé :
Dependency Parsing is one of the basic tasks in the field of Natural Language Processing (NLP). The goal is to find whether there exist a strong relationship between different words in a sentence. It can be used as the basic step of many NLP systems like question answering system. Solving a dependency parsing problem can be realized by a energy based network with the output of the neural network as a scalar (energy). The goal is to find the most compatible structure (a graph) with the input sentence and the most compatible structure is supposed to give the lowest energy for the neural network. As the structure of the sentence should be a tree (one root, every word has and only has one pa rent, no circle), to simplify the problem, people always construct a linear function corresponding to the structure that we want to find, i.e. we suppose different arcs are independent. However, this method may limit the capacity of the system to describe more complex relations. In this project, inspired by the idea of Structure Prediction Energy Network (SPEN), we construct a new neural network which is composed of two parts, i.e. local energy part and global energy part. We showed that it is possible to solve the problem with dual decomposition when we have a convex (non-linear) function for the global energy part together with the linear local energy part. As one part of my Phd thesis, this work is still ongoing.
 28/02/2019 Apprentissage statistique dans un contexte décentralisé et applications à la vision par ordinateur, par David Picard
 David Picard, ENSEA Cergy-Pontoise
Salle B107, bâtiment B, Université de Villetaneuse
28/02/2019    12:15 - 13:45
Résumé :
L'apprentissage statistique est de nos jours incontournable dans un certain nombre de tâches complexes, notamment dans le traitement des données multimédia comme la vision. Pour gagner en précision, des modèles de plus en plus complexes sont entraînés sur des volumes de données de plus en plus gros. Cependant, la répartition naturelle des données auprès des capteurs qui les ont crées laisse à penser qu'il serait préférable d'apprendre ces modèles sans collecter les données d'apprentissage auprès d'un calculateur central. Nous présentons dans cet exposé un paradigme d'apprentissage décentralisé asynchrone pour répondre à ce problème. Nous considérons le cas ou plusieurs calculateurs optimisent un modèle statistique à l'aide de données locales et coopèrent afin d'obtenir un modèle consensus. Nous montrons comment transposer des algorithmes d'apprentissage connus (k-means, PCA, SVM, deep learning) à ce paradigme, ainsi que des preuves de leur équivalence avec les versions centralisées. Enfin, nous montrons plusieurs exemples d'applications de ces modèles à des tâches de vision par ordinateur.
 27/02/2019 Monoides et algèbres de tris sur les groupes de coxeter, par Nicolas Thiéry
 Nicolas Thiéry
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Nicolas Thiéry (Université Paris 11).

Le modèle combinatoire usuel pour décrire la 0-algèbre de Hecke H_n(0) (en type A) est de considérer l'algèbre (ou le monoïde) engendré par les opérateurs de tri-à-bulle élémentaires pi_i, i=1...n-1 définis comme suit: pi_i agit sur un mot de longueur n en triant les lettres en position i et i+1. Cette construction se généralise naturellement pour tout groupe de Coxeter fini.

En combinant ces opérateurs avec plusieurs variantes (tri croissant / décroissant / affine), nous construisons un certain nombre de monoïdes et algèbres. De manière étonnante en premier abord, ceux-ci se retrouvent munis d'une structure très riche, faisant intervenir la combinatoire des descentes (et une généralisation de celle-ci), les ordres usuels sur les groupes de Coxeter (Bruhat, permutohèdre gauche et droit), ainsi que de nouveaux ordres. Cette structure s'explique par de nombreuses connections avec la théorie des représentations, l'algèbre de Hecke affine, les fonctions symétriques, etc.

 27/02/2019 Une formalisation des actes de language en ludique (et quelques remarques générales sur l'utilisation de la logique en shs), par s et Samuel Tronçon
 s et Samuel Tronçon
B 311, LIPN
27/02/2019    15:22 -
Résumé :

Les séminaires LCR et RCLN accueillent Samuel Tronçon (Centre d'Epistémologie et d'Ergologie Comparative et Institut de Mathématiques de Luminy).

Nous proposons une formalisation des actes de langage dans le cadre formel de la Ludique. Nous définissons un acte de langage ludique (ALL) comme une structure exécutable apte à remplir certains tests, et dont l'interaction produit une modification du contexte. Notre modèle possède deux couches de représentation. La première, la plus primitive, est constituée par les interactions en contexte. Elle comprend donc les structures qui supportent l'acte de langage. La seconde, plus abstraite, est le résultat de catégorisations réalisées par les agents, sur la base des interactions réelles entre actes de langage et avec le contexte. Cette double articulation ouvre la voie à la prise en compte du caractère relatif des actes en fonction de sa structure, du contexte et de l'observateur.

 27/02/2019 (annulé pour cause de grève) une formalisation des actes de langage en ludique" (et quelques remarques générales sur l'utilisation de la logique en shs), par s et Samuel Tronçon
 s et Samuel Tronçon
B311
27/02/2019    15:22 -
Résumé :

(ANNULE pour cause de GREVE)

Les séminaires LCR et RCLN accueillent Samuel Tronçon (Institut de Mathématiques de Luminy et Paris 8).

Nous proposons une formalisation des actes de langage dans le cadre formel de la Ludique. Nous définissons un acte de langage ludique (ALL) comme une structure exécutable apte à remplir certains tests, et dont l'interaction produit une modification du contexte. Notre modèle possède deux couches de représentation. La première, la plus primitive, est constituée par les interactions en contexte. Elle comprend donc les structures qui supportent l'acte de langage. La seconde, plus abstraite, est le résultat de catégorisations réalisées par les agents, sur la base des interactions réelles entre actes de langage et avec le contexte. Cette double articulation ouvre la voie à la prise en compte du caractère relatif des actes en fonction de sa structure, du contexte et de l'observateur.

 27/02/2019 La plateforme why de vérification déductive de programmes c et java, par J.C. Filliâtre.
 J.C. Filliâtre.
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Jean-Christophe Filliâtre (CNRS Université Paris 11).

Cet exposé présente la plateforme Why (http://why.lri.fr/), un ensemble de techniques et d'outils développés dans le projet ProVal pour la vérification de propriétés fonctionnelles de codes C et Java. La plateforme Why s'appuie sur plusieurs principes :
(1) la spécification des programmes par l'intermédiaire d'annotations dans le source, en utilisant des langages inspirés de JML ;
(2) un calcul de plus faibles préconditions reposant sur un modèle mémoire de type Burstall-Bornat raffiné par une analyse statique de séparation ; et enfin
(3) la possibilité d'utiliser un grand nombre d'outils de preuve existants, tant automatiques qu'interactifs, pour décharger les obligations de preuve.

 27/02/2019 (annulé pour cause de grève) monoides et algèbres de tris sur les groupes de coxeter, par N. Thiéry
 N. Thiéry
B311
27/02/2019    15:22 -
Résumé :

(ANNULE pour cause de GREVE)

Le séminaire LCR accueille Nicolas Thiéry (Université Paris 11).
(Travail commun avec Florent Hivert et Anne Schilling)

Le modèle combinatoire usuel pour décrire la 0-algèbre de Hecke H_n(0) (en type A) est de considérer l'algèbre (ou le monoïde) engendré par les opérateurs de tri-à-bulle élémentaires pi_i, i=1...n-1 définis comme suit: pi_i agit sur un mot de longueur n en triant les lettres en position i et i+1. Cette construction se généralise naturellement pour tout groupe de Coxeter fini.

En combinant ces opérateurs avec plusieurs variantes (tri croissant/décroissant/affine), nous construisons un certain nombre de monoïdes et algèbres. De manière étonnante en premier abord, ceux-ci se retrouvent munis d'une structure très riche, faisant intervenir la combinatoire des descentes, ainsi que les ordres usuels sur les groupes de Coxeter (Bruhat, permutohèdre gauche et droit). Cette structure s'explique en fait par de nombreuses connections avec la théorie des représentations, l'algèbre de Hecke affine, les fonctions symétriques, etc.

 27/02/2019 Fractional calculus: definitions, numerical methods and applications in control systems and multi-Scale processes, par Z. Odibat
 Z. Odibat
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Zaid Odibat (Al-Balqa' Applied University, Jordan).

Recently, the fractional derivative has drawn much attention due to its wide application in various fields of physics and engineering. Fractional derivatives provide an excellent instrument for the description of memory and hereditary properties of various materials and processes. The main reason for using the integer-order models was the absence of solution methods for fractional differential equations. The real objects of using fractional-order models are that we have more degrees of freedom in the model and that a memory is included in the model. Fractional-order systems have an unlimited memory.

In this presentation, we will, first, introduce the most used definitions of fractional derivatives and their properties then we will highlight some comments about differential equations of fractional order. Second, we will give an overview of the recent analytical-approximate methods that are used to provide approximate solutions for nonlinear differential equations of fractional order. Finally, we will introduce some important areas of applications, where the use of fractional order models is expected to be very suitable and useful. Theses areas included the control systems and the multi-scale processes.

 27/02/2019 An introduction to size-Change termination analysis, par A. Ben-Amram
 A. Ben-Amram
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Amir Ben-Amram(The Academic College of Tel-Aviv).

This talk describes an approach to the problem of determining whether a program terminates for all input data.

The basic idea of Size-Change Termination (SCT) is to prove that in any (hypothetic) infinite computation by the program, an infinite descent in some data arises. When the data considered are drawn from a well-founded set (typically the natural numbers), infinite descent is impossible, and the logical conclusion is: no actual computation path can be infinite.

The approach subsumes the usual methods of proving termination by observing that "something decreases" in each loop, e.g., lexicographic descent of a tuple of variables.

But how can the desired property be proven? The SCT technique relies on Size Change Graphs, a convenient abstraction of program behaviour. Using these graphs, it is possible to formulate the condition of interest in combinatorial terms, which helped to get several results, the first of which was that the property is decidable.

Subsequent work identified the complexity class of the problem (complete for PSPACE), investigated different algorithms (including efficient approximations), showed how to abstract different kinds of programs (functional, imperative, high-order, TRS...), and a lot more. This talk will be mostly introductory and include a brief exposition of results from the research of the speaker and his colleagues.

 27/02/2019 Réécriture, catégories d'ordre supérieur, et expressivité des modèles de calcul concurrent, par D. Mazza
 D. Mazza
B311
27/02/2019    15:22 -
Résumé :
Le séminaire LCR accueille Damiano Mazza (LIPN).

Un problème fondamental dans la comparaison de différents modèles du parallélisme et de la concurrence est celui de définir la notion de codage, ou de traduction. A ce jour, parmi toutes les notions universellement acceptées de codage entre modèles concurrents, il n'en existe aucune qui s'impose nettement sur les autres. Nous proposons d'étudier la notion de codage en partant de la vision du calcul comme réécriture, et en utilisant des notions venant de la théorie des catégories d'ordre supérieur et de la théorie des structures d'évenements de Winskel.

 27/02/2019 Descriptions algébriques et logiques de graphes finis, par B. Courcelle
 B. Courcelle
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Bruno Courcelle (Labri).

De manière à étendre aux graphes les concepts fondamentaux de la Théorie des Langages Formels, on définit sur l'ensemble des graphes finis deux structures d'algèbre (de "magma" selon une terminologie obsolète) qui généralisent la structure de monoïde libre. On en déduit de manière immédiate des notions de reconnaissabilité (par congruences finies) et d'algébricité (par systèmes d'équations à points fixes) pour les graphes , et de nombreuses propriétés prouvables au niveau algébrique.

L'expression de propriétés de graphes en Logique du Second-Ordre Monadique permet de concrétiser la notion d'ensemble reconnaissable de graphes, de même que les automates finis concrétisent celle de langage reconnaissable (de mots ou de termes). Cette logique permet aussi d'étendre la notion de transduction rationnelle et de famille génératrice pour les 2 types d'ensembles équationnels considérés.

Il en résulte de nombreux résultats en particulier : algorithmes FPT pour ces propriétés, le paramètre étant la largeur arborescente ou "de clique", théorèmes de filtrage pour les ensembles équationnels de graphes et résultats de décidabilité associés, constructions effectives des mineurs exclus.

 27/02/2019 Calcul logique pour multiséquents, par C. Fouqueré
 C. Fouqueré
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Christophe Fouqueré (LIPN).

Un Calcul logique gérant des multiséquents est présenté. Ce calcul est motivé par une réflexion sur l'évaluation paresseuse en programmation logique, ou encore la concurrence stricte et l'interférence. Le calcul introduit deux nouveaux connecteurs gérant la structure de multiséquents. C'est une extension conservative de la Logique Linéaire, permettant l'élimination des coupures. On proposera une sémantique des phases. Si le temps le permet, on évoquera des extensions du calcul.
 27/02/2019 Fonctions parfaitement non linéaires et actions de groupe, par L. Poinsot
 L. Poinsot
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Laurent Poinsot (LIPN).

Les boîtes-S des procédés de chiffrement (à clef secrète) par blocs itéré sont notamment conçues pour résister aux attaques différentielle et linéaire. Ces cryptanalyses reposent sur la manière de combiner le texte clair et la clef. L'opération de combinaison traditionnellement employée est l'addition bit-à-bit de vecteurs binaires. Il existe d'autres façons de mélanger le clair et la clef, aussi dans cet exposé on se propose de remplacer l'addition par une action de groupe plus générale. On étudie alors l'attaque différentielle adaptée à cette nouvelle opération de combinaison ainsi que les boîtes-S qui lui opposent la meilleure résistance possible. On montre en particulier que l'on peut construire des fonctions robustes dans des cas où leurs homologues classiques (i.e. lorsque l'opération de combinaison est une addition binaire) n'existent pas.
 27/02/2019 Petit voyage au pays de la programmation logique inductive, par C. Rouveirol
 C. Rouveirol
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Céline Rouveirol (LIPN).

Je présenterai une brève introduction à la Programmation Logique Inductive, qui s'intéresse aux modèles logique de l'apprentissage supervisé et plus largement à l'apprentissage supervisé dans les langages de concepts restrictions de la logique d'ordre un. Je motiverai ce type d'apprentissage, je détaillerai les modèles logiques les plus utilisés en Programmation Logique Inductive et quelques travaux fondateurs, pour enfin pointer vers quelques problématiques prometteuses.
 27/02/2019 Exponentials in ludics: how and at what price, par M. Basaldella
 M. Basaldella
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Michele Basaldella (Università di Siena).

Ludics is a research project introduced by J-Y Girard in 2001 whose aim is to overcome the distinction Syntax/Semantics (of proofs) and it consists of a theory in which both sides deal with objects of the same nature, Design, which are basic artifacts of Ludics. They are manipulated by means of cut-elimination, conceived as the unique tool for testing properties inside the theory itself. Ludics also provides a (fully complete) Game Semantics for Multiplicative Additive Focalized Linear Logic. In this talk, we will show how to extend Ludics framework by adding exponential constructions in such a way to preserve the Ludics Theorems (in particular Separation Theorem). As we will see, our approach is closely related to AJM Game Semantics in the treatment of exponentials. We will also discuss the limits of our framework as well as its strength, namely the preservation of all isomorphisms involving exponentials, and the arising of a notion of non uniform exponential, both appearing in a rather natural way.
 27/02/2019 Modular construction of the symbolic observation graph, par L. Petrucci
 L. Petrucci
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Laure Petrucci (LIPN).

Model checking for Linear Time Logic (LTL) is usually based on converting the (negation of a) property into a Büchi automaton, composing the automaton and the model, and finally checking for emptiness of the language of the composed system. The last step is the crucial stage of the verification process because of the state explosion problem. In this work, we present a solution which builds, in a modular way, an observation graph represented in a non-symbolic manner but where the nodes are essentially symbolic sets of states and the edges either labeled by events occurring in the formula or by synchronization actions between the system components. Due to the small number of events to be observed in a typical formula, this graph has a very moderate size and thus the time complexity for verification is negligible w.r.t. the time to build the observation graph. Experimental results show that our method outperforms both a non-modular generation of the symbolic graph and existing non-symbolic approaches (modular or not).
 27/02/2019 Mc-Sog: an ltl model checker based on symbolic observation graphs, par K. Klai
 K. Klai
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Kais Klai (LIPN).

Model checking is a powerful and widespread technique for the verification of finite distributed systems. However, the main hindrance for wider application of this technique is the well-known state explosion problem. During the last two decades, numerous techniques have been proposed to cope with the state explosion problem in order to get a manageable state space. Among them, on-the-fly model-checking allows for generating only the "interesting" part of the model while symbolic model-checking aims at checking the property on a compact representation of the system by using Binary Decision Diagram (BDD) techniques. In this work, we propose a technique which combines these two approaches to check LTL\X state-based properties over finite systems. During the model checking process, only an abstraction of the state space of the system, namely the symbolic observation graph, is (possibly partially) explored. The building of such an abstraction is guided by the property to be checked and is equivalent to the original state space graph of the system w.r.t. LTL\X logic (i.e. the abstraction satisfies a given formula f iff the system satisfies f). Our technique was implemented for systems modeled by Petri nets and compared to an explicit model-checker as well as to a symbolic one (NuSMV) and the obtained results are very competitive.
 27/02/2019 Correctness of multiplicative additive proof structures is nl-Complete, par P. Jacobé de Naurois
 P. Jacobé de Naurois
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Paulin Jacobé de Naurois (LIPN).

We revisit the correctness criterion for the multiplicative additive fragment of linear logic. We prove that deciding the correctness of corresponding proof structures is NL-complete. (Joint work with V. Mogbil).
 27/02/2019 L'interaction dure, par S. Lippi
 S. Lippi
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Sylvain Lippi (I3S, Université de Nice).

Les systèmes durs, une sous-classe des réseaux d'interaction, se présentent sous la forme de systèmes de re-étiquetage de graphes fortement confluents. Nous présentons quelques traductions dans des sous-classes des systèmes durs et en déduisons quelques idées simples sur l'universalité. En particulier, nous donnons une traduction dans un système universel à 7 règles.
 27/02/2019 Réécriture de la géométrie, par Yves lafont
 Yves lafont
B107
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Yves lafont (IML - Université de la Méditerranée) en B107. Notez la salle inhabituelle.

Ce travail (en collaboration avec Pierre Rannou), vaguement inspiré par la recherche sur le calcul quantique, s'inscrit dans un programme de recherche plus vaste intitulé Â« Géométrie de la réécriture Â». On représente les matrices orthogonales réelles (ou les isométries de $$\mathbb{R}^n$$) par des Â« circuits orthogonaux Â» construits avec deux types de portes : la symétrie (porte unaire) et les rotations (portes binaires). On obtient ainsi un système de réécriture de diagrammes qui est à la fois noetherien et confluent. La forme normale généralise la Â« décomposition d'Euler Â». La confluence est évidente, mais l'étude des paires critiques conduit à une description axiomatique de la fonction permettant de passer d'une décomposition d'Euler à l'autre en dimension 3. En particulier, on retrouve l'Â« équation du tétraèdre Â», aussi appelée équation de Zamolodchikov, bien connue des physiciens théoriciens.

Référence : Y. Lafont, Towards an Algebraic Theory of Boolean Circuits, Journal of Pure and Applied Algebra 184 (2-3), p. 257-310, Elsevier (2003).

 27/02/2019 Construction et maintenance d'entrepôts de données, par F. Boufares & co
 F. Boufares & co
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille pour une heure : Faouzi Boufares (LIPN), Sana Hamdoun (LIPN) et Mohamed Badri (CRIP5 - LIPN - Université Paris 5).

Les données nécessaires à des fins décisionnels sont de plus en plus complexes. Elles ont des formats hétérogènes et proviennent de sources distribuées. Elles peuvent être classées en trois catégories : les données structurées, les données semi-structurées et les données non-structurées. Dans cet exposé, nous présentons le processus d'intégration de données dans le but de construire un entrepôt dont les sources sont totalement hétérogènes. Nous proposons un cadre formel qui se base sur la définition d'un environnement d'intégration. Nous présentons également notre processus de maintenance d'entrepôt de données qui assure à la fois la mise à jour du contenu de l'entrepôt et l'actualisation des agrégats (indicateurs décisionnels) calculés sur les données de l'entrepôt.
 27/02/2019 Semantics for higher-Order quantum computation, par Benoît Valiron
 Benoît Valiron
B107
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Benoît Valiron (University of Ottawa).

We give a categorical semantics for a call-by-value linear, computational lambda calculus and discuss some steps towards a concrete model. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is its linear type system, which includes a duplicability operator "!" as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements.

 27/02/2019 From universal algebra and topology to lambda calculus and back, par Antonino Salibra
 Antonino Salibra
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille (en première partie d'une séance double) Antonino Salibra (Università Ca'Foscari di Venezia)

In this seminar we show how algebra and topology can be fruitfully applied to the operational semantics and to the model theory of the untyped lambda calculus. We explain the structure of the lattice of lambda theories (i.e., equational extensions of lambda calculus) and analyze one of the long-standing open problem of lambda calculus, regarding the existence of a topological model of the beta-eta lambda theory, where all Scott-continuous functions are representable.

 27/02/2019 Extraction de programmes classique dans le calcul des constructions, par Alexandre Miquel
 Alexandre Miquel
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille (en deuxième partie de cette séance double) Alexandre Miquel (PPS - Université Paris 7)

Dans cet exposé, je me propose de montrer que les techniques de réalisabilité classique introduites par Jean-Louis Krivine sont compatibles avec le Calcul des Constructions avec univers (CCw), et qu'elles permettent d'envisager un mécanisme d'extraction de programme à partir de preuves classiques (avec proof-irrelevance et axiome du choix) formalisées en Coq (dans la sorte Prop).

Pour cela, je commencerai par rappeler ce qu'est la réalisabilité classique au sens de Krivine (langage et modèles). Ensuite je montrerai comment étendre le modèle de réalisabilité de Krivine (initialement défini pour l'arithmétique du second ordre) à CCw, en utilisant une structure de Î -set réminiscente des structures de -set (Hyland, Longo, Moggi), de D-set (Streicher) et de Î»-set (Altenkirch). Enfin, je présenterai un certain nombre de pistes pour étendre ce schéma d'extraction aux types inductifs (notamment les entiers) en utilisant des structures de données efficaces dans le langage cible (entiers binaires).

 27/02/2019 Le monoïde partiel libre, par Laurent Poinsot
 Laurent Poinsot
B311
27/02/2019    15:22 -
Résumé :

Le séminaire LCR accueille Laurent Poinsot (LIPN, Université Paris 13).

La structure de monoïde est fondamentale en informatique théorique, et plus précisément en combinatoire algébrique, puisqu'elle est reliée aux concepts de langages, d'automates, de séries formelles et d'algèbres de Lie combinatoires par exemple.

Un monoïde est un ensemble non vide muni d'une loi de composition interne associative et d'un élément neutre bilatère. De façon informelle, un monoïde partiel est un monoïde dont la loi de composition n'est que partiellement défini. Un monoïde à zéro est un monoïde (total) pourvu d'un élément distingué, le zéro, qui est absorbant pour sa loi de composition interne.

Dans cet exposé, après avoir effectué des rappels concernant ces différentes structures ainsi que des notions de théorie des catégories, je montre que les catégories des monoïdes à zéro et des monoïdes partiels sont essentiellement identiques (le zéro marque l'erreur d'un produit non défini), et qu'elles diposent d'un objet libre, à savoir, le monoïde partiel libre, généralisant en cela le résultat classique concernant l'existence du monoïde (total) libre.

 27/02/2019 Focalisation et ludique, par Alexis Saurin
 Alexis Saurin
B311
27/02/2019    15:22 -
Résumé :

Le 18 janvier 2010, à 15h30 en salle B311, le séminaire LCR accueille Alexis Saurin (PPS - INRIA Î R2).

La propriété de Focalisation est l'un des résultats essentiels de la théorie de la démonstration de la logique linéaire, mettant en évidence le rôle essentiel de la polarité en logique. La Focalisation est la source de développements importants, allant de la programmation logique linéaire aux approches interactives de sémantiques de jeux.  La ludique, quant à elle, est un formalisme logique introduit par Girard il y a une dizaine d'années dont l'élément de base est la notion d'interaction.

L'exposé que je présenterai est le résultat d'une collaboration avec Basaldella et Terui, du RIMS à Kyoto. Terui a revisité récemment la théorie Ludique de Girard en y apportant de nouvelles perspectives, notamment selon l'aspect calculatoire, sous le nom de computational Ludics. Je présenterai une analyse interactive du théorème de focalisation menée dans le cadre de la Ludique de Terui.

J'expliquerai également les motivations de ce travail provenant de la remarque que la propriété de focalisation peut être vue comme reliée à des résultats de théorie de la complexité, notamment de compression de bande pour des Machines de Turing.

 27/02/2019 Mancoosi: reliable upgrades and quality assurance in foss distributions, par Stefano Zacchiroli
 Stefano Zacchiroli
B311
27/02/2019    15:22 -
Résumé :

Le 15 février 2010, à 15h30 en salle B311, le séminaire LCR accueille Stefano Zacchiroli (PPS).

FOSS (Free and Open Source Software) distributions are rather peculiar instances of component-based software infrastructures: they are developed rapidly and without "tight" central coordination, they are huge (tens of thousands of components), and their importance in the Internet computing infrastructure is growing.

Both the construction of a coherent collection of components (or packages), and the maintenance of installations based on these, raise difficult problems for distribution maintainers and system administrators. Distributions evolve rapidly by releasing new versions of packages and strive for increasingly high quality assurance requirements on their component collections. System upgrades may proceed on different paths depending on the current state of the system and the available software packages, and system administrators are faced with choices of upgrade paths (often unappropriately hidden), and with frequent upgrade failures.

The ongoing project Mancoosi (Managing the Complexity of the Open Source Infrastructure) aims to solve some of these problems. We will describe current and past work in the context of Mancoosi, as well as some future research directions.

 27/02/2019 Finite automata and regular fixed point formulas in mumall, par David Baelde
 David Baelde
B311
27/02/2019    15:22 -
Résumé :

Le 11 janvier 2010, à 15h30 en salle B311, le séminaire LCR accueille David Baelde (University of Minnesota, USA).

We present muMALL, an extension of multiplicative additive linear logic with least and greatest fixed points, and illustrate its expressiveness through the model-checking problem of non-deterministic finite automata inclusion.

We consider encoding automata as least fixed points in muMALL, and use its general induction scheme to reason about them. We provide a coinductive characterization of inclusion that yields a natural bridge to proof-theory. This yields a completeness theorem, but can also be generalized to the fragment of "regular formulas", obtaining new insights about inductive theorem proving and cyclic proofs in particular.

 27/02/2019 Une intégration de la sémantique lexicale à la sémantique compositionnelle montagovienne, par Christian Retoré
 Christian Retoré
B311
27/02/2019    15:22 -
Résumé :

Le 25 janvier 2010, à 15h30 en salle B311, le séminaire LCR accueille Christian Retoré (LaBRI -- Université de Bordeaux et CNRS, INRIA Bordeaux Sud-Ouest).

Les modèles formels de la sémantique du langage naturel sont relativement pauvres et méconnus si on les compare à ceux utilisés pour sa syntaxe. La sémantique de Montague, plutôt satisfaisante du point de vue formel, reste  incapable d'exprimer la polysémie ou les relations entre significations. A  l'autre extrême, les sémantiques lexicales sans structures, et en particulier sans structure  argumentale, n'ont pas de règles de composition pour calculer la signification d'entités composées. Nous avons proposé une notion de lexique sémantique  dans la lignée du lexique génératif de J. Pustejovsky comme un raffinement de la sémantique de R. Montague: en plus du lambda-terme usuel représentant la structure argument d'un mot, le lexique associe aussi des lambda-termes permettant au mot de changer son type et d'être relié à ses autres significations possibles. Le lambda-calcul du second ordre est utilisé pour anticiper les changements de type dépendant des types affectés aux autres mots. Ceci fournit un algorithme correct de calcul du sens d'expressions composées, que ce soit en utilisant les aspects pertinents du sens lors de la composition (qualia exploitation) ou en produisant exactement les sens correspondants à des coprédications possibles et en bloquant celles qui ne le sont pas --- ce que les modèles proposés jusqu'ici ne faisaient pas automatiquement.

On peut ainsi traiter d'exemples comme:
(1) un sourire amoureux et interrogatif (c'est l'auteur du sourire et non le sourire lui même qui est amoureux et  s'interroge)
(2) Le thon que nous  avons mangé hier était vif comme l'éclair et délicieux (coprédication quasi impossible entre l'animal et la nourriture)
(3) Copenhague est à la fois un port et une capitale cosmopolite (coprédication très acceptable entre le lieu, l'institution et les personnes)

Pour conclure nous procéderons à notre autocritique et expliquerons  comment des systèmes de types plus raffinés issus de la logique linéaire pourraient constituer un juste milieu entre l'approche présentée où types et termes sont trop indépendants et celle de N. Asher où les termes sont dictés par les types: linguistiquement est clair que seuls certains types permettent l'existence  de transformateurs de types, mais que leur existence dépend de la langue et de l'entrée lexicale considérée.

[Travail réalisé avec Christian Bassac (Lyon) et Bruno Mery (Bordeaux)]

Références bibliographiques:
Towards a Type-Theoretical Account of Lexical Semantics
Bassac C., Mery B., Retoré C.
Journal of Logic Language and Information (2009)
http://hal.archives-ouvertes.fr/docs/00/40/83/08/PDF/bassac-mery-retore-revised.pdf

 27/02/2019 Types et effets : des monades aux réseaux différentiels. 1ère partie : régions, stratification, monades, par Paolo Tranquilli
 Paolo Tranquilli
B311
27/02/2019    15:22 -
Résumé :

Le 1er février 2010, à 13h30 (attention à l'horaire inhabituel !) en salle B311, le séminaire LCR accueille Paolo Tranquilli (ENS Lyon).

Les systèmes de types et effets permettent une analyse statique des effets de bord des programmes. Par exemple, en considérant la mémoire comme un ensemble de régions, on peut annoter le type d'une procédure qui accède à des variables globales avec l'ensemble des régions affectées. Récemment, des systèmes de types et effets à régions stratifiées ont été proposés pour assurer la terminaison de lambda-calculs avec références (partagées entre plusieurs threads).

Mon exposé partira d'un autre outil utilisé pour traiter les effets : les monades de Moggi sont une notion de théorie catégorique qui peut être utilisée en théorie des types pour "enrober" les effets en gardant le système "pur". La monade d'état TA = S (SA) permet de modéliser l'accès à la mémoire ; en outre, en paramétrant S avec les régions, on peut facilement traduire le lambda-calcul (séquentiel) avec types et effets dans le lambda-calcul avec paires. On arrive alors à une justification purement logique de la stratification : son absence est en fait équivalente au besoin d'utiliser des types récursifs.

La traduction se transfère aisément aux réseaux de preuve de la logique linéaire, à partir de la traduction du lambda-calcul par valeur (la deuxième traduction de Girard). Les réseaux donnent une réduction parallèle du calcul qui en préserve la sémantique séquentielle. On pourra alors passer au travail en cours, qui mène à étendre cette traduction au calcul multi-threaded en utilisant les réseaux différentiels. La traduction, qui utilise les zones de communications déjà exploité pour le pi-calcul, donne une simulation, mais les réseaux obtenus ne sont pas nécessairement corrects comme dans le cas séquentiel. On est donc obligé soit de restreindre le calcul concurrent, soit d'étudier des extensions des réseaux ou des modifications de leur critère de correction.

 27/02/2019 Quelques thèmes de la théorie de la démonstration du xxe siècle, vus d'ajourd'hui, par Cycle de séminaires théorie de la démonstration, Abrusci-Vauzeilles
 Cycle de séminaires théorie de la démonstration, Abrusci-Vauzeilles
B311
27/02/2019    15:22 -
Résumé :

Dans la période de février à avril 2010, Vito Michele Abrusci (Università Roma Tre, professeur invité au LIPN) et Jacqueline Vauzeilles (LIPN) proposent un cycle de séminaires sur

Quelques thèmes de la théorie de la démonstration du XXe siècle, vus d'ajourd'hui

Le cycle est composé de quatre séances, ouvertes à tous, qui se tiendront au LIPN en salle B311, avec le calendrier suivant :
• 15 février 2010, 13h30-15h : Hilbert
• 22 février 2010, 13h30-16h30 : ordinaux et notations ordinales
• 22 mars 2010, 13h30-16h30 : Gentzen et omega-logique
• 19 avril 2010, 13h30-16h30 : beta-logique
 27/02/2019 Types et effets : des monades aux réseaux différentiels. 2ème partie, par Paolo Tranquilli
 Paolo Tranquilli
B311
27/02/2019    15:22 -
Résumé :

Le 1er mars 2010, à 13h30 (attention à l'horaire inhabituel !) en salle B311, le séminaire LCR accueille Paolo Tranquilli (ENS Lyon).

Les systèmes de types et effets permettent une analyse statique des effets de bord des programmes. Par exemple, en considérant la mémoire comme un ensemble de régions, on peut annoter le type d'une procédure qui accède à des variables globales avec l'ensemble des régions affectées. Récemment, des systèmes de types et effets à régions stratifiées ont été proposés pour assurer la terminaison de lambda-calculs avec références (partagées entre plusieurs threads).

Mon exposé partira d'un autre outil utilisé pour traiter les effets : les monades de Moggi sont une notion de théorie catégorique qui peut être utilisée en théorie des types pour "enrober" les effets en gardant le système "pur". La monade d'état TA = S  (S A) permet de modéliser l'accès à la mémoire ; en outre, en paramétrant S avec les régions, on peut facilement traduire le lambda-calcul (séquentiel) avec types et effets dans le lambda-calcul avec paires. On arrive alors à une justification purement logique de la stratification : son absence est en fait équivalente au besoin d'utiliser des types récursifs.

La traduction se transfère aisément aux réseaux de preuve de la logique linéaire, à partir de la traduction du lambda-calcul par valeur (la deuxième traduction de Girard). Les réseaux donnent une réduction parallèle du calcul qui en préserve la sémantique séquentielle. On pourra alors passer au travail en cours, qui mène à étendre cette traduction au calcul multi-threaded en utilisant les réseaux différentiels. La traduction, qui utilise les zones de communications déjà exploité pour le pi-calcul, donne une simulation, mais les réseaux obtenus ne sont pas nécessairement corrects comme dans le cas séquentiel. On est donc obligé soit de restreindre le calcul concurrent, soit d'étudier des extensions des réseaux ou des modifications de leur critère de correction.

 27/02/2019 Modélisation du protocole neoppod, par Sami Evangelista
 Sami Evangelista
B311
27/02/2019    15:22 -
Résumé :

Le 1er mars 2010, à 15h30 en salle B311, le séminaire LCR accueille Sami Evanglista (LIPN).

 27/02/2019 Jump from parallel to sequential proofs: exponentials, par Paolo Di Giamberardino
 Paolo Di Giamberardino
B311
27/02/2019    15:22 -
Résumé :

Le 26 avril 2010, à 13h30 en salle B311, le séminaire LCR accueille Paolo Di Giamberardino (LIPN).

In previous works, by importing ideas from game semantics (notably Faggian-Maurel-Curien's ludics nets), we defined a new class of multiplicative/additive polarized proof nets, called J-proof nets. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by using jumps (that is, untyped extra edges) as sequentiality constraints. Starting from this result, in the present work we extend J-proof nets to take into account erasing (weakening) and duplication (contraction). More precisely, we show how using jumps makes possible to define nets where the usual nesting condition on boxes is relaxed, allowing a partial superposition of boxes. Moreover, we prove that, even in case of ''superposed'' boxes, reduction still enjoys confluence and strong normalization, using Gandy's method to prove strong normalization, following the work of Pagani and Tortora de Falco.

 27/02/2019 Un langage de programmation orienté interaction, par Jean-Louis Giavitto
 Jean-Louis Giavitto
B311
27/02/2019    15:22 -
Résumé :

Le 26 avril 2010, à 15h30 en salle B311, le séminaire LCR accueille Jean-Louis Giavitto (IBISC, CNRS-Université Evry).

Plusieurs formalismes informatiques tentent de capturer la notion d'interaction dans un système. MGS, un langage de programmation expérimental, est fondé sur la constatation que l'ensemble des interactions possibles s'organise suivant une structure topologique simple qui permet de spécifier la description du système et son évolution. Le style de programmation qui en résulte, la programmation spatiale, s'appuie sur des relations topologiques (connexité, bord, obstruction...) pour renouveler la notion de structure de données et a trouvé des applications effectives en algorithmique, en intelligence artificielle, dans la modélisation et la simulation en biologie des systèmes et dans la programmation des systèmes autonomes.

http://mgs.spatial-computing.org/

 27/02/2019 Game semantics and applications to compilation (3/3): A type system for hard real-time computation, par Dan Ghica
 Dan Ghica, University of Birmingham
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 11:30
Résumé :
We will examine a type system, suitable for higher-order functional programming languages with mutable state, which can automatically certify the timing of execution. The system is generally applicable to hard real-time computation and especially to the automatic synthesis of computational pipelines. We present the general typing rules, a categorical semantic model and a proof of coherence as well as a concrete programming language with a type inference algorithm and a concrete game-semantic model. [Joint work with Alex Smith]
 27/02/2019 Categorical models for simply typed resource calculi, par Giulio Manzonetto
 Giulio Manzonetto
D214
27/02/2019    15:22 -
Résumé :

Le 12 avril 2010, à 15h30 en salle D214 (attention à la salle inhabituelle !), le séminaire LCR accueille Giulio Manzonetto (LIPN).

In this talk we will present two resource sensitive lambda-calculi. The first one is the resource calculus, a non-lazy version of Boudol's lambda calculus with multiplicities.

In this calculus there are two kinds of resources: intuitionistic ones that can be erased and copied, and linear ones that must be used exactly once.

The second calculus is Ehrhard and Reignier's differential lambda calculus. In this calculus there are two kinds of applications: the usual application of lambda calculus and a linear application. This last one is useful to define a syntactical derivative operator on terms. We will see that these two calculi are strongly linked and that - in particular - the resource calculus can be easily translated into the differential one.

Subsequently, we will provide sufficient conditions on Blute-Cockett-Seely's Cartesian differential categories for being categorical models of the differential lambda calculus (and of the resource calculus by translation).

Finally, we will see that the concrete categories previously introduced as models of these calculi are instances of this abstract definition.

 27/02/2019 La sémantique relationnelle de la logique linéaire est-Elle injective?, par Daniel de Carvalho
 Daniel de Carvalho
D214
27/02/2019    15:22 -
Résumé :

Le 12 avril 2010, à 13h30 en salle D214 (attention à la salle inhabituelle !) le séminaire LCR accueille Daniel de Carvalho (LIPN).

Pour un certain fragment de la logique linéaire, la relation d'équivalence sur les preuves induite par l'élimination des coupures coïncide avec celle induite par le modèle relationnel basé sur les multi-ensembles.

 27/02/2019 Tour d'horizon de la programmation réactive, par Daniele Terreni
 Daniele Terreni
B311
27/02/2019    15:22 -
Résumé :

Le 10 mai 2010, à 15h30 en salle B311, le séminaire LCR accueille Daniele Terreni (LIPN).

Les systèmes réactifs sont des systèmes qui interagissent de façon intense avec leur environnement. Ils reçoivent des stimulations et doivent y réagir promptement. Selon la nature de l'environnement, leur réaction peut être soumise à des contraintes sur le temps d'exécution ou la quantité de mémoire utilisée. D'autre part, lorsque plusieurs interactions avec l'environnement sont possibles en même temps, ce qui est un cas typique, la nature de ces systèmes devient concurrente.

D'un point de vue mathématique, ces systèmes peuvent être décrits par des équations : les portions de l'état global sont des variables et ces variables obéissent à un ensemble d'équations récursives. Cet approche, très déclarative, paraît séduisante pour le programmeur : en spécifiant les invariants du système, il aura aussi décrit son implémentation.

Dans ce tour d'horizon, nous nous concentrerons sur les domaines d'application sans contraintes de temps ou de mémoire. Nous explorerons quelques langages conçus pour ces systèmes par des petits exemples de programmation. Nous essayerons de comprendre comment ces langages dépassent les limites des méthodes traditionnelles d'implémentation telles que les threads asynchrones ou les boucles évènementielles.

 27/02/2019 Church => scott = ptime: an application of resource sensitive realizability, par Aloïs Brunel
 Aloïs Brunel
B311
27/02/2019    15:22 -
Résumé :

Le 17 mai 2010, à 15h30 en salle B311, le séminaire LCR accueille Aloïs Brunel (ENS Lyon).

We introduce DIAL_lin, a dual variant of intuitionistic linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. Recasting an older result of Leivant and Marion, we give a characterization of the complexity class PTIME as the functions representable by a lambda-term of type 'Church' => 'Scott', where 'Church' is the type of usual Church binary words and 'Scott' the type of Scott words (a purely linear representation of words).

We will focus on the technique used to prove the soundess part of this result. It is a variant of the Dal Lago and Hofmann's realizability framework, which both gives meaning to the logic and allows us to bound the runtime of any typable lambda-term. We will discuss the possible extensions and simplification of this construction.

 27/02/2019 Graphes d'interaction, par Thomas Seiller
 Thomas Seiller
B311
27/02/2019    15:22 -
Résumé :

Le 31 mai 2010, à 15h30 en salle B311, le séminaire LCR accueille Thomas Seiller (IML, Aix-Marseille 2).

Je présenterai une sémantique localisée du fragment multiplicatif de la logique linéaire (MLL) où les preuves sont représentées par des graphes. Cette sémantique, inspirée des derniers travaux de J.-Y. Girard, se révèle être une version combinatoire de la géométrie de l'interaction dans le facteur hyperfini. Elle permet en particulier de mettre en rapport ces récents développements et les réseaux de preuves, les sémantiques de jeu ou la ludique. Je discuterai également d'une généralisation au fragment multiplicatif-additif de la logique linéaire (MALL).

 27/02/2019 How and why purely propositional separation logic is undecidable, par Max Kanovich
 Max Kanovich
B311
27/02/2019    15:22 -
Résumé :

Le 5 juillet 2010, à 15h30 en salle B311, le séminaire LCR accueille Max Kanovich (Queen Mary University of London).

Separation logic developed by Reynolds and O'Hearn has proven as an adequate formalism for the analysis of programs that manipulate memory (in the form of pointers, heaps, stacks, etc.). In addition to the standard propositional connectives, the most important feature of separation logic is its separating conjunction (A*B) which holds for a heap h iff h can be split into separate h1 and h2 so that A holds for h1 and B holds for h2.

Here our main focus is on the logic for concrete heap-like models of practical interest. Whatever concrete heap-like model H we take, it is undecidable whether a purely propositional formula A is valid in this model H. We also prove undecidability for a number of natural propositional systems (Boolean BI, Classical BI, etc.) developed on the road towards axiomatization of separation logic.

On top of that, our undecidability results for concrete heap-like models give new insights into the nature of decidable fragments of separation logic such as those given by Calcagno-Yang-O'Hearn(2001) and Berdine-Calcagno-O'Hearn(2004), as well as imposing boundaries on decidability.

To add a new exhibit to the Undecidability Zoo, we show the simplest undecidable purely propositional system, we call it Minimal BI, which employs only two conjunctions, that is * and &, and their two adjoint implications, respectively. (Neither negation nor `false' should be blamed for its undecidability)

This is joint work with James Brotherston (Imperial)

 27/02/2019 Linear dependent types and intensional expressivity, par Marco Gaboardi
 Marco Gaboardi
B311
27/02/2019    15:22 -
Résumé :

Le 20 septembre 2010, à 15h30 en salle B311, le séminaire LCR accueille Marco Gaboardi (Università di Bologna).

I present a work in progress, joint work with Ugo Dal Lago, aiming at providing a general framework for implicit computational complexity. By means of dependent types  and dependent modality in a linear setting we can formally reflect at the type level the program evaluation complexity. This fact allow us to obtain implicit characterizations of complexity classes that are complete in terms of programs, reducing the class membership problem to a corresponding constraint satisfaction problem.

 27/02/2019 Un calcul de coercitions qui prouve la normalisation forte de mlf, par Paolo Tranquilli
 Paolo Tranquilli
B311
27/02/2019    15:22 -
Résumé :

Le 15 novembre 2010, à 15h30 en salle B311, le séminaire LCR accueille Paolo Tranquilli (LIP, ENS Lyon).

Je présenterai un travail en collaboration avec Giulio Manzonetto qui montre la normalisation forte d'MLF par une simulation dans le système F. MLF est une extension conservative de ML qui permet de programmer tous le termes du système F à l'aide d'annotations partielles de type. Dans une première partie je vais décrire MLF, et notamment xMLF, sa variante explicite en style Church. Dans xMLF les relations d'instance des types sont explicitement notés par des entités nommées "instantiations" qui jouent en fait un rôle de coercitions et qui se réduisent de façon non triviale. Pour mieux raisonner sur ces aspects de xMLF on va le traduire dans une décoration du système F, le calcul de coercitions Fc, qui abstrait le mécanisme de coercition. On va donc présenter ce calcul et montrer que l'effacement des coercitions qui plonge Fc dans le lambda calcul ordinaire est une bisimulation faible. Finalement on va définir la traduction de xMLF dans Fc et utiliser la bisimulation pour montrer la normalisation forte des autres variantes de MLF aussi.

 27/02/2019 Full abstraction for resource calculus with tests, par Giulio Manzonetto
 Giulio Manzonetto
B311
27/02/2019    15:22 -
Résumé :

Le 22 novembre 2010, à 15h30 en salle B311, le séminaire LCR accueille Giulio Manzonetto (Nijmegen).

In this seminar we present a fully abstract model of the resource calculus "with tests".

We will first shortly recall the full resource calculus à la Tranquilli together with its relational model D, and we will define the problem of full-abstraction in this context.

We will then show that D is also a model of a resource calculus extended with two unary operators (similar to "raise" and "catch" of programming languages) and parallel composition |. With these operators (arising from differential proofnets) we can define "tests" that are able to check whether a term of the resource calculus converge.

We will then associate each element sigma in the interpretation of a term M with a context C_sigma converging on M and diverging on terms "different" from M. This will give us the full abstraction result.

 27/02/2019 Une critique de la notion d'information en biologie et un modèle de la complexité phénotypique au cours de l'évolution comme anti-Entropie, par Giuseppe Longo
 Giuseppe Longo
B311
27/02/2019    15:22 -
Résumé :

Le 29 novembre 2010, à 15h30 en salle B311, le séminaire LCR accueille Giuseppe Longo (LIENS, CNRS-ENS Paris).

The major observables in Physics are largely, if not exclusively, based on or derived from energy (conservation properties as symmetries, geodetic principles as least action principles...). Biology forced us to think in the novel terms of organization and, even, of inherited organization; an organization whose complexity grows along evolution and embryogenesis, against energy degradation in Physics (entropy production, also in non-isolated systems).

Then, with World War II, the age of coding, decoding and information started. Informatics, Information Theory and Cryptography became well defined scientific displines, with their own principles and remarkable applications. Can we borrow for the analysis of life phenomena any relevant principle or precise result from these scientific areas? A critique of the abuse of Information in Biology will be hinted.

Some recent work will be introduced on a quantification of biological (phenotypic) organization by a proper observable to Biology, anti-entropy. The idea will be derived by conceptual dualities w. r. to Quantum Physics, where the operatorial approach by Schrödinger to his famous equation will (dually) guide us towards an equational modelling of Goulds analysis of phenotypic complexity along Darwins Evolution and, if time allows, to some applications to embryogenesis.

 27/02/2019 Higher order processes and soft logic, par Simone Martini
 Simone Martini
B311
27/02/2019    15:22 -
Résumé :

Le 13 décembre 2010, à 15h30 en salle B311, le séminaire LCR accueille Simone Martini (Bologne, Professeur invité à Paris 13).

I will discuss an application of light/soft linear logic technology to restrict the higher order pi-calculus. In this restricted calculus any process terminates in polynomial time. While several interesting processes are expressible, more work is needed to understand a satisfactory way of describing "resource bounded" processes.

 27/02/2019 Functional programming in sublinear space, par Ugo Dal Lago
 Ugo Dal Lago
B311
27/02/2019    15:22 -
Résumé :

Le 20 décembre 2010, à 15h30 en salle B311, le séminaire LCR accueille Ugo Dal Lago (Bologne).

We consider the problem of functional programming with data in external memory, in particular as it appears in sublinear space computation. Writing programs with sublinear space usage often requires one to use special implementation techniques for otherwise easy tasks, e.g. one cannot compose functions directly for lack of space for the intermediate result, but must instead compute and recompute small parts of the intermediate result on demand. We study how the implementation of such techniques can be supported by functional programming languages.

 27/02/2019 Algebraic type systems, par Alejandro Di­az Caro
 Alejandro Di­az Caro
B311
27/02/2019    15:22 -
Résumé :

Le 17 janvier 2011, à 15h30 en salle B311, le séminaire LCR accueille Alejandro Di­az Caro (LIG, Grenoble).

In this talk I will present several extensions to the System F, for the sake of type the linear-algebraic lambda-calculus, a lambda-calculus enriched with a vectorial structure. The first type system is a straightforward extension of System F, which just types the calculus without any further adornment. The second one is a type system accounting for scalars, which can serve as a guarantee that the normal form of a term is of the form \sum a_i.t_i with \sum a_i=1. The following system includes "sums of types" reflecting that of the terms--showing that sums in the algebraic calculus behaves as a special kind of pairs. Eventually the last type system combines the previous two. We give counterexamples of why this kind of vectorial type system cannot be made in Curry style and show the clues of a future vectorial type system in Church style suitable to specialize the calculus into a quantum calculus.

 27/02/2019 On quantum lambda calculi, par Margherita Zorzi
 Margherita Zorzi
B311
27/02/2019    15:22 -
Résumé :

Le 7 février 2011, à 15h30 en salle B311, le séminaire LCR accueille Margherita Zorzi (Università di Verona).

In this talk we will introduce some theoretical results about quantum lambda calculi. Starting from a measurement-free calculus, called Q, we will show some "standard" properties (such as congruence and subject reduction) and some quantum properties, focusing on the expressive power and on the relationship with other quantum computational models.

Successively, we will consider Q*, an extension of Q with an explicit measurement operator, and we will propose a confluence result for reductions sequences regardless their niteness.

Finally, we will propose an ICC-like approach for the quantum setting: we will spend some words about a sub-calculus of Q, called SQ, which captures the three classes of the quantum polytime.