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

Afficher les séminaires de

Séminaires à venir
LOVE 08/09/2023 Compositional Verification of Embedded Real-Time Systems, par Mohammed Foughali
Mohammed Foughali, IRIF  
Salle B107, bâtiment B, Université de Villetaneuse
08/09/2023    12:15 - 13:30
Résumé :
In an embedded real-time system (ERTS), real-time tasks (software) are typically executed on a multicore shared-memory platform (hardware). The number of cores is usually small, contrasted with a larger number of complex tasks that share data to collaborate. Since most ERTSs are safety-critical, it is crucial to rigorously verify their software against various real-time requirements under the actual hardware constraints (concurrent access to data, number of cores). Both the real-time systems and the formal methods communities provide elegant techniques to realize such verification, which nevertheless face major challenges. For instance, model checking (formal methods) suffers from the state-space explosion problem, whereas schedulability analysis (real-time systems) is pessimistic and restricted to simple task models and schedulability properties. In this paper, we propose a scalable and generic approach to formally verify ERTSs. The core contribution is enabling, through joining the forces of both communities, compositional verification to tame the state-space size. To that end, we formalize a realistic ERTS model where tasks are complex with an arbitrary number of jobs and critical sections, then show that compositional verification of such model is possible, using a hybrid approach (from both communities), under the state-of-the-art partitioned fixed-priority (P-FP) with limited preemption scheduling algorithm. The approach consists of the following steps, given the above ERTS model and scheduling algorithm. First, we compute fine-grained data sharing bounds for each critical section that reads or writes some data from the shared memory. Second, we generalize an algorithm that, aware of the data sharing bounds, computes an affinity (task-core allocation) guaranteeing the schedulability of hard-real-time (HRT) tasks. Third, we devise a timed automata (TA) model of the ERTS, that takes into account the affinity, the data sharing bounds and the scheduling algorithm, on which we demonstrate that various properties can be verified compositionally, \ie on a subset of cores instead of the whole ERTS, therefore reducing the state-space size. In particular, we enable the scalable computation of tight worst-case response times (WCRTs) and other tight bounds separating events on different cores, thus overcoming the pessimism of schedulability analysis techniques. We fully automate our approach and show its benefits on three real-world complex ERTSs, namely two autonomous robots and on an automotive case study from an industrial challenge.
Séminaires passés
LOVE 12/05/2023 MUPPAAL: Reducing and Removing Equivalent and Duplicate Mutants in UPPAAL, par James Ortiz
James Ortiz, Université de Namur  
Salle B107, bâtiment B, Université de Villetaneuse
12/05/2023    12:15 - 13:15
Résumé :
Mutation Testing (MT) is a test quality assessment technique that creates mutants by injecting artificial faults into the system and evaluating the ability of tests to distinguish these mutants. We focus on MT for safety-critical Timed Automata (TA). MT is prone to equivalent and duplicate mutants, the former having the same behaviour as the original system and the latter other mutants. Such mutants bring no value and induce useless test case executions. We propose MUPPAAL, a tool that: (1) offers a new operator reducing the occurrence of mutant duplicates; (2) an efficient bisimulation algorithm removing remaining duplicates; (3) leverages existing equivalence-avoiding mutation operators. Our experiments on four UPPAAL case studies indicate that duplicates represent up to 32% of all mutants and that the MUPPAAL bisimulation algorithm can identify them more than 99% of the time.
LOVE 13/04/2023 The cartesian closed bicategory of thin spans , par Simon Forest
Simon Forest, Aix-Marseille Université  
Salle B107, bâtiment B, Université de Villetaneuse
13/04/2023    10:30 - 11:30
Résumé :
In the Rel model of linear logic, types are interpreted by sets, and proofs/programs by relations. A natural idea to have a quantitative, or proof-relevant model (i.e. a model that keeps distinct the different executions giving rise to the same observable result), is to use spans instead of relations. Indeed the (bi)category Span, whose morphisms are spans of sets composed by pullbacks, can be seen as a proof-relevant analogue: where a relation between A and B keeps only binary information (if a and b are related), a span associates to all a and b a set of witnesses, or "proofs" that they are related. Unfortunately, a naive adaptation of exponential on Rel does not work on Span. Other works, such as those on generalized species of structure, provide proof-relevant models, but where the composition requires a complex quotient of the witnesses, thus lacking the "concrete" aspect of the pullback. Although a quotient seems unavoidable, another model, the one of "thin concurrent games", involves a concrete composition, without quotient. By adapting the techniques used in the latter model, this work gives good results in the direction of a span model of LL, where the composition is done by classical pullbacks. In particular, it is shown that, for an adequate pseudocomonad on spans, we obtain a cartesian closed co-Kleisli bicategory.
AOC 04/04/2023 Reformulations pour l'optimisation convexe par morceaux, par Renan Spencer Trindade
Renan Spencer Trindade, LIX - Ecole Polythecnique  
Salle B107, bâtiment B, Université de Villetaneuse
04/04/2023    10:30 - 11:30
Résumé :
La programmation non linéaire en nombres entiers (PNLNE) a fait l'objet d'une attention croissante de la part des chercheurs ces dernières années en raison de sa capacité à modéliser une grande variété d'applications dans le monde réel. Cependant, obtenir un optimum global d'un problème PNLNEs non convexes reste très difficile. Il est donc primordial d'exploiter, quand possible, toutes les propriétés mathématiques des PNLNE qu'on souhaite résoudre. Notre étude est motivée par la résolution de PNLNE lorsque le non-convexité se manifeste par la somme de fonctions univariées non convexes. Nous proposons une méthode basée sur des relations PNLNE convexes, obtenues en traitant séparément les intervalles où chaque fonction univariée est convexe ou concave. Dans la relaxation PNLNE convexe, chaque intervalle concave est remplacé par une linéarisation par morceaux. Pour résoudre le PNLNE résultant, nous utilisons une méthode de plans coupants qui utilise des coupes perspectives. Pour atteindre l'optimum globale, la précision de la relaxation de l'intervalle concave est incrémentée de manière itérative. Ce processus nécessite l'introduction de nouvelles variables binaires pour l'activation des intervalles dans lesquels les fonctions sont définies. Toutefois, cette étape de reformulation peut en fait être réalisée de différentes manières. Dans notre travail, nous comparons les trois différentes formulations classiques tant sur le plan théorique que sur le plan pratique. Nous prouvons que, contrairement au cas linéaire, les formulations ne sont pas équivalentes lorsque la reformulation en perspective est appliquée. Nous montrons l'impact des différentes formulations par des résultats de calcul.
AOC 23/03/2023 Exact algorithms for linear matrix inequalities and application to the moment problem, par Simone Naldi
Simone Naldi, Université de Limoges  
Salle B107, bâtiment B, Université de Villetaneuse
23/03/2023    10:30 - 11:30
Résumé :
In this talk I will discuss computer algebra algorithms for solving exactly linear matrix inequalities, that is, the feasibility of a semidefinite program. These algorithms rely on the determinantal structure behind SDP. The main motivation is for certifying lower bounds in polynomial optimization, for instance, for computing the sum of squares certificates of multivariate polynomials. Recently a new application to the so-called truncated moment problem gives new perspectives that will be discussed in the second part of the talk. This consists of the decision problem whether a sequence of real numbers, indexed by monomials of degree d in n variables, is the moment sequence of a nonnegative Borel measure with support in some basic semialgebraic set. This is based on joint work with D. Henrion and M. Safey El Din.
AOC 22/03/2023 Two non-linear stochastic problems with catastrophic consequences, par Alberto Santini
Alberto Santini, ESSEC  
Salle B107, bâtiment B, Université de Villetaneuse
22/03/2023    10:30 - 11:30
Résumé :
We study two stochastic problems in which some events occur with low probability but can have catastrophic consequences. The first is the 0-1 Time-bomb Knapsack Problem, an extension of the classical Knapsack Problem in which each item has an associated probability of exploding and destroying the entire content of the knapsack. The objective is to maximise the expected profit of the selected items. The second is the Hazardous Orienteering Problem (HOP), which extends the classical Orienteering Problem. In the HOP, the vehicle picks up parcels at the customers it visits. Some of these parcels have a probability of exploding and destroying the entire content of the vehicle. This probability depends on the amount of time the parcel spends on board the vehicle, following an exponential distribution. The objective is again to maximise the expected collected profit. We propose mathematical formulations and valid inequalities, exact algorithms based on branch-and-bound and dynamic programming, and primal and dual bounding techniques for both problems.
RCLN 20/03/2023 From Language Models to (very) Large Language Models, par Davide Buscaldi
Davide Buscaldi, LIPN (équipe RCLN)  
Salle B107, bâtiment B, Université de Villetaneuse
20/03/2023    12:30 - 14:30
Résumé :
Originairement destiné à l'équipe RCLN, je propose ce séminaire pour tous les curieux sur les derniers modèles de langage, BERT, GPT, GPT-2, GPT-3, GPT-4 et bien sûr chatGPT. J'ai ciblé la presentation pour couvrir aussi les bases des modèles de langage pour comprendre le fonctionnement de ces modèles à plus bas niveau.
LOVE 17/03/2023 Weak omega-categories and their internal language in dependent type theory, par Thibaut Benjamin
Thibaut Benjamin, CEA List  
Salle B107, bâtiment B, Université de Villetaneuse
17/03/2023    14:00 - 15:00
Résumé :
Weak omega-categories are one of the most difficult algebraic structures to define and study, because of the large number axioms that they require. I will present the language CaTT, introduced by Finster and Mimram in order to describe weak omega-categories. I will first use an implementation of the theory to write a few definition in this language, in order to provide intuition on the kind of structure that we consider and get used to the language. Then I will describe this language formally as a dependent type theory and hint at a formal presentation of weak omega-category. Finally I will discuss a few improvements that can be made to the language and relate the syntactic manipulations to the semantic interpretation in weak omega-category theory
LOVE 16/03/2023 Knowledge and Topology: Simplicial Models for Epistemic Logic, par Jérémy Ledent
Jérémy Ledent, University of Strathclyde  
Salle B107, bâtiment B, Université de Villetaneuse
16/03/2023    10:30 - 11:30
Résumé :
Multi-agent Epistemic Logic is a modal logic of knowledge. It allows to reason about a finite set of agents who may know facts about the world, and about each other. In this talk, I will present a new semantics for epistemic logic, based on simplicial complexes. In this approach, the knowledge of the agents is modeled by a higher-dimensional space called a simplicial model; and the satisfaction of an epistemic logic formula can be evaluated by inspecting the various possible paths in this space. I will illustrate these ideas using examples from the theory of distributed computing, where the agents correspond to processes that can exchange information in order to solve a task. Both topological invariants and logical invariants can be leveraged to prove that some distributed computing tasks are impossible to solve.
AOC 16/03/2023 Robust min-max regret covering problems, par Amadeu Almeida Coco
Amadeu Almeida Coco  
Salle B107, bâtiment B, Université de Villetaneuse
16/03/2023    10:30 - 10:30
Résumé :
This presentation discusses two min-max regret covering problems: the min-max regret Weighted Set Covering Problem (min-max regret WSCP) and the min-max regret Maximum Benefit Set Covering Problem (min-max regret MSCP). These problems are the robust optimization counterparts, respectively, of the Weighted Set Covering Problem and of the Maximum Benefit Set Covering Problem. In both problems, uncertainty in data is modeled by using an interval of continuous values, representing all the infinite values every uncertain parameter can assume. This study has the following major contributions: (i) a proof that MSCP is ?p2-Hard, (ii) a mathematical formulation for the min-max regret WSCP, (iii) exact and (iv) heuristic algorithms for the min-max regret WSCP and the min-max regret MSCP. We reproduce the main exact algorithms for the min-max regret WSCP found in the literature: a Logic-based Benders decomposition, an extended Benders decomposition, and a branch-and-cut. In addition, such algorithms have been adapted for the min-max regret MSCP. Moreover, five heuristics are applied for both problems: two scenario-based heuristics, a path relinking, a pilot method, and a linear programming-based heuristic. The goal is to analyze the impact of such methods on handling robust covering problems in terms of solution quality and performance.
AOC 10/03/2023 Partial Optimality in Cubic Correlation Clustering, par Silvia Di Gregorio
Silvia Di Gregorio, Faculty of Computer Science TU Dresden  
Visio - https://bbb.lipn.univ-paris13.fr/b/wol-ma9-vjn - 514019
10/03/2023    12:00 - 13:00
Résumé :
The higher-order correlation clustering problem is an expressive model, and recently, local search heuristics have been proposed for several applications. Certifying optimality, however, is NP-hard and practically hampered already by the complexity of the problem statement. Here, we focus on establishing partial optimality conditions for the special case of complete graphs and cubic objective functions. In addition, we define and implement algorithms for testing these conditions and examine their effect numerically, on two datasets.
AOC 09/03/2023 Catégories de sommets pour le problème de domination , par Vincent Bouquet
Vincent Bouquet, CNAM  
Salle B107, bâtiment B, Université de Villetaneuse
09/03/2023    10:30 - 11:30
Résumé :
Cette présentation porte sur les sommets qui appartiennent à tous les ensembles dominants minimums d'un graphe. Nous caractérisons ces sommets en fonction de leur criticité relativement au nombre de domination. Cette criticité mesure comment le retrait d'un sommet du graphe affecte le nombre de domination. Nous nous intéressons ensuite à cette caractérisation dans quelques classes de graphes: les graphes triangulés, les cographes, ainsi que des sous-classes des graphes sans griffe. Pour ces graphes, nous montrons que les sommets persistants sont toujours critiques: c'est-à-dire que le retrait d'un sommet persistant fait augmenter le nombre de domination.
COMP 06/03/2023 Operator Scaling II, par Thomas Seiller
Thomas Seiller, CNRS, LIPN  
Hybride (Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
06/03/2023    14:30 - 16:00
Résumé :
COMP 27/02/2023 Random SAT, par Alexandros Singh
Alexandros Singh, LIPN  
Hybride (Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
27/02/2023    14:30 - 16:00
Résumé :
COMP 20/02/2023 Descriptive Complexity, par Paulin de Naurois
Paulin de Naurois, CNRS, LIPN  
Hybride (Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
20/02/2023    14:30 - 16:00
Résumé :
AOC 16/02/2023 Multiplicité dans le partitionnement de graphes signés, par Nejat Arinik
Nejat Arinik, INRAE  
Salle B107, bâtiment B, Université de Villetaneuse
16/02/2023    10:30 - 11:30
Résumé :
Selon la théorie de l'équilibre structural, un graphe signé est structurellement équilibré s'il peut être partitionné en sous-groupes mutuellement hostiles (i.e. reliés seulement par des liens négatifs) tout en exhibant une solidarité interne (i.e. contenant uniquement des liens positifs). Mais un réseau réel (i.e. un graphe représentant un système du monde réel) est rarement parfaitement équilibré : on trouvera quelques liens positifs entre les groupes et/ou quelques liens négatifs à l'intérieur de certains groupes. L'un des défis du domaine est de quantifier le niveau de déséquilibre d'un tel réseau et d'identifier les liens qui causent ce déséquilibre. Le problème Correlation Clustering (CC) se définit précisément par l'obtention d'une partition possédant un déséquilibre minimal. Le partitionnement de graphes signés constitue une tâche importante du point de vue applicatif, étant donné que trouver une partition équilibrée aide à comprendre le système modélisé par le graphe signé. Cependant, l'approche standard dans la littérature se contente de chercher une seule partition, comme si elle caractérisait suffisamment le système étudié. Or, on peut avoir besoin de plusieurs partitions pour construire une image plus juste du système étudié. Même si cette notion de la multiplicité est extrêmement important du point de vue des utilisateurs finaux, elle a été très peu abordée dans la littérature. Une particulière situation dans laquelle on veut relaxer l'hypothèse de partition unique et en chercher plusieurs est lié au problème CC. Quand on résout une instance de ce problème, plusieurs partitions optimales peuvent coexister. La question qui se pose est de savoir ce qu'on perd, si on considère une seule partition optimale, alors qu'il en existe plusieurs. Idéalement, il faut les énumérer toutes avant de faire une analyse concluante. Pour ce faire, on propose une nouvelle méthode d'énumération et un framework basé sur l'analyse de clustering afin de d'abord complètement énumérer l'espace des partitions optimales, puis étudier empiriquement un tel espace. Nos résultats ont révélé une typologie de l'espace de partitions optimales : 1) une seule partition optimale ; 2) quelques partitions constituant une seule classe ; 3) beaucoup de partitions optimales constituant une seule classe de forme allongée ; 4) plusieurs partitions optimales constituant plusieurs classes de partitions.
RCLN 13/02/2023 Towards Detecting Pre-training Data Set Manipulations: the Need to Build Efficient Language Models, par Wissam Antoun
Wissam Antoun, INRIA  
Salle B107, bâtiment B, Université de Villetaneuse
13/02/2023    12:30 - 13:30
Résumé :
The high compute cost required to train Large Language Models (LLMs) makes them only available to a hand full of high-budget private institutions, and countries. These institutions rarely documented their training data nor the data collection and filtering source code, thus raising questions about potential vulnerabilities of models that have been trained on them. For example, one of the many ways to inject adversarial biases and temper with training data is to produce machine-generated text carrying out these biases and have them included in the training data. So the matter of robust detection of machine-generated text is becoming crucial. Answering these questions first requires efficient ways to iterate and train language models quickly. In this talk, I will present my work on pretraining language models for Arabic and French and showcase the lessons learned in designing and training efficient LLMs. In particular, I'll talk about training AraBERT, AraELECTRA, AraGPT2, the current largest Transformer-based models for Arabic, and the AraGPT2 detector. I’ll also introduce CamemBERTa, a new sample-efficient language model for French, the first publicly available DeBERTa V3-based model outside of the original paper and which establishes a new SOTA for this language in many tasks. (Joint work with Benoit Sagot and Djamé Seddah, at the Inria’s Almanach team project)
LOVE 09/02/2023 Non-deterministic abstract machines, par Sergueï Lenglet
Sergueï Lenglet, Loria, Université de Lorraine  
Salle B107, bâtiment B, Université de Villetaneuse
09/02/2023    10:30 - 11:30
Résumé :
We present a generic design of abstract machines for non-deterministic programming languages such as process calculi or concurrent lambda calculi. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way. We show how to automatically derive a non-deterministic abstract machine from a zipper semantics - a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics.
AOC 09/02/2023 QP/NLP-based Branch-and-Bound algorithm for MINLP: It could work! , par Luca Mencarelli
Luca Mencarelli, ENSTA  
Salle B107, bâtiment B, Université de Villetaneuse
09/02/2023    10:30 - 11:30
Résumé :
We describe a novel QP/NLP-based Branch-and-Bound algorithm for convex MINLP. Then, we introduce a tailored version of the previous algorithm for (non-convex) Binary Nonlinear Optimization Problems (BNPs), relying on a simple convexification procedure and a tailor convex quadratic under-approximation. We survey computational experiences on convex instances of MINLPLib and on several literature and random generated instances for BNPs.
AOC 08/02/2023 Hamiltonian degree condition for tough graphs, par Cleophee Robin
Cleophee Robin, Université de Montreal Canada  
https://bbb.lipn.univ-paris13.fr/b/wol-ma9-vjn - code: 514019
08/02/2023    16:00 - 17:00
Document attaché
Résumé :
A graph G is hamiltonian if there exists a G cycle containing all G vertices exactly once. A graph G is t-tough if, for all subsets of vertices S, the number of connected components in G-S is at most |S|/t. We extended the Theorem of Hoàng by proving the following: Let G be a graph with degree sequence d_1,d_2, ..., d_n, and let t be a positive integer at most 4. If G is a t-tough and if for each i, t <= i < n/2, d_i <= i --> d_{n-i+t} >= (n - i) then G is hamiltonian. To do this we extend the closure lemma due to Bondy and Chvàtal.
LOVE 02/02/2023 Call-by-value in bicategories of games , par Hugo Paquet
Hugo Paquet, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
02/02/2023    10:30 - 11:30
Résumé :
Game semantics is naturally described using a bicategory, rather than a category, because the composition of strategies is only associative and unital up to isomorphism. This makes it difficult to relate game semantics to the categorical theories of effects and resources, developed by Moggi, Melliès, and many others. In this talk I will describe new notions in bicategory theory: strong pseudomonads and premonoidal bicategories, that can be used for the semantics of call-by-value languages. As the main motivating example, I will discuss the bicategorical structure of game semantics and the universal properties that we can use to prove the coherence axioms. This is based on joint work with Philip Saville.
COMP 30/01/2023 Matrix scaling I, par Thomas Seiller
Thomas Seiller, CNRS, LIPN  
Hybride (Salle B107 & https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
30/01/2023    14:30 - 16:00
Résumé :
I will talk about matrix/ operator scaling and how it relates to perfect matchings and polynomial identity testing.
COMP 16/01/2023 Optimisation problems, par Bruno Escoffier
Bruno Escoffier, LIP6  
Hybride (Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
16/01/2023    14:30 - 15:30
Résumé :
LOVE 12/01/2023 Introduction to Coherent Differentiation, par Aymeric Walch
Aymeric Walch, IRIF  
Salle B107, bâtiment B, Université de Villetaneuse
12/01/2023    10:00 - 12:00
Résumé :
The differential lambda calculus was introduced by Ehrhard and Reigner, following from the discovery of finitness spaces by Ehrhard. In those models of linear logic, a morphism !X -> Y can be seen as an analytic function. Analytic functions can always be written as an infinite sum involving the interrated derivatives (in the sense of the usual differential calculus) thanks to the so called Taylor Expansion. Ehrhard and Reigner transposed those ideas on the syntactic side. They introduced a syntactical notion of differentiation, corresponding to a notion of substitution in which only one occurence of a variable is replaced. They also introduced a syntactical counterpart for Taylor expansion. The major issue of differential calculus though is its non determinism, embodied by the Leibniz rule of differential calculus. There a multiple ways to substitute exactly one occurrence of a variable inside a given term. This non deterministic choice is represented by the use of formal sums and, on the side of models, the category is required to be additive (that is, enriched over commutative monoids). It leaves behind many models of LL, such as coherence spaces and probabilistic coherent spaces. Coherent Differentiation was introduced by Ehrhard in 2021 in order to solve those issues. In coherent differentiation, two morphisms are not always assumed to be summable. Interestingly, the notion of summability can be seen as some kind of strong Monad on the category, and the axioms of differentiation turn out to be necessary and sufficient conditions that allows to extends this Monad to the co-Kleisli category of the exponential. The goal of this talk is to introduce those ideas, with an emphasis on how coherent differentiation is a conservative extension of differential logic.
LOVE 15/12/2022 Synchronous and spatialized computations with Global Transformations, par Alexandre Fernandez
Alexandre Fernandez, ENS Lyon  
Salle B107, bâtiment B, Université de Villetaneuse
15/12/2022    10:30 - 12:00
Résumé :
This presentation outlines some ideas of my PhD about Global Transformations. These form a general method to describe local and synchronous spatialized dynamical systems such as Cellular Automata and Lindenmayer systems. This work originated from the goal of extending such systems to dynamical graphs. This talk first introduces the categorical formalism, and providing examples of such systems over different structures such as words or graphs. It also give simple instances of many categorical constructions, such as comma categories, colimits and Kan extensions. These tools are then used to relate the local specification of a system and its global behavior. The extension of this formalism to non-deterministic computations is then considered.
COMP 12/12/2022 On the weakness of logarithmic depth algebraic circuits, par Ulysse Léchine
Ulysse Léchine, LIPN, Université Paris 13  
Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy
12/12/2022    16:00 - 16:30
Résumé :
Talk planned as part of the ANR DySCo launch meeting.
COMP 12/12/2022 Lower bounds in Algebraic complexity, par Sébastien Tavenas
Sébastien Tavenas, CNRS, LAMA (Université Savoie Mont-Blanc)  
Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy
12/12/2022    14:30 - 15:30
Résumé :
Talk planned as part of the ANR DySCo launch meeting.
LOVE 09/12/2022 Vers des Processus Métier Corrects basés sur la Blockchain, par Ikram Garfatta
Ikram Garfatta, Équipe LoVe, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
09/12/2022    12:30 - 13:30
Résumé :
Plusieurs caractéristiques de la technologie Blockchain sont bien alignées sur des questions critiques dans le domaine de la gestion des processus métier (BPM), et pourtant l'adoption de Blockchain pour le BPM ne doit pas être prise à la légère. En effet, la sécurité des contrats intelligents, qui sont l'un des principaux éléments de la blockchain rendant possible son intégration avec le domaine BPM, s'est révélée vulnérable. Il est donc crucial pour la protection des processus métier conçus de prouver l'exactitude des contrats intelligents à déployer sur une blockchain. Dans cet exposé, je présenterai les travaux qui ont été menés au cours de ma thèse de doctorat, et dont l'objectif est d'apporter des contributions dans le contexte susmentionné. En effet, nous proposons une approche formelle basée sur la transformation des contrats intelligents Solidity, en tenant compte du contexte BPM dans lequel ils sont utilisés, en un réseau de Petri coloré hiérarchique. Nous exprimons un ensemble de vulnérabilités des contrats intelligents sous forme de formules de la logique temporelle linéaire et utilisons le vérificateur de modèle Helena non seulement pour détecter ces vulnérabilités tout en discernant leur exploitabilité, mais aussi pour vérifier d'autres propriétés spécifiques aux contrats. L'approche que nous proposons est basée sur la vérification des modèles CPN et comprend principalement trois phases : 1) la transformation du code Solidity des contrats intelligents en sous-modèles CPN correspondant à leurs fonctions. 2) transformer le contexte BPM en un modèle CPN 3) la construction d'un modèle CPN en fonction d'une propriété LTL qui peut exprimer : i) une vulnérabilité dans le code, ou ii) une propriété spécifique au contrat, en le reliant à un modèle CPN représentant le comportement à considérer, et l'utilisation du vérificateur de modèles pour vérifier la propriété ciblée sur le modèle construit.
LOVE 08/12/2022 Bidirectional Typing : From a Nice Implementation Technique to a Powerful Theoretical Tool, par Meven Lennon-Bertrand
Meven Lennon-Bertrand, University of Cambridge  
Salle B107, bâtiment B, Université de Villetaneuse
08/12/2022    14:00 - 15:00
Résumé :
In 2000, Pierce and Turner introduced a new technique called local type inference, to perform type inference for ML-like languages. The key idea was to carefully understand the flow of information in a typing derivation. This idea was not isolated: similar techniques had appeared independently in quite a few other contexts. The general idea, which came to be referred to as bidirectional typing, was in particular a cornerstore idea in the folklore of implementers of dependently typed languages. But it turns out that bidirectional typing is not just a nice implementation technique. It is also an interesting theoretical tool when working on the properties of type systems. In this talk, I will try and give some of my understanding of bidirectional typing, and how it can be used to make the infamously difficult meta-theory of dependent type systems a bit less difficult.
LOVE 02/12/2022 Exploring a Parallel SCC Algorithm: Using TLA+ and the TLC Model Checker, par Jaco van de Pol
Jaco van de Pol, Aarhus University + University of Twente  
Salle B107, bâtiment B, Université de Villetaneuse
02/12/2022    13:15 - 14:00
Résumé :
We explore a parallel SCC-decomposition algorithm based on a concurrent Union-Find data structure. In order to increase confidence in the algorithm, it is modelled in TLA+. The TLC model checker is used to demonstrate that it works correctly for all possible interleavings of two workers on a number of small input graphs. To increase the understanding of the algorithm, we investigate some potential invariants. Some of these are refuted, revealing that the algorithm allows suboptimal (but still correct) executions. Finally, we investigate some modifications of the algorithm. It turns out that most modifications lead to an incorrect algorithm, as revealed by the TLC model checker. We view this exploration as a first step to a full understanding and a rigorous correctness proof based on invariants or step-wise refinement. As ongoing work, we try to verify the correctness of the algorithm for any number of workers on any input graph, using the TLPAM proof manager.
LOVE 02/12/2022 A Rewriting Logic Semantics and Statistical Analysis for Probabilistic Event-B, par Daniel Osorio
Daniel Osorio, Équipe LoVe, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
02/12/2022    12:15 - 13:00
Résumé :
Formal methods provide a general structure for specifying real world systems as abstract models with mathematical rigor, that can be proven to be correct and implemented as specific pieces of software or hardware. Some systems must operate amid uncertain information, hence the need for probabilistic models where specific behaviors can be proved to be present or absent up to a certain confidence threshold. Event-B is a proof-based formal method for discrete systems modeling, and it has been extended to cope with probabilistic behaviors. To be able to do simulations and probabilistic temporal verification of probabilistic Event-B models, we present a rewriting logic semantics for probabilistic Event-B. The approach takes as input a probabilistic Event-B specification, and outputs a probabilistic rewrite theory that is fully executable in PMaude and can be statistically tested against quantitative metrics, using statistical model checking tools like MultiVeStA.
AOC 01/12/2022 Smoothed analysis of the simplex method, par Sophie Huiberts
Sophie Huiberts  
https://bbb.lipn.univ-paris13.fr/b/wol-ma9-vjn - code: 514019
01/12/2022    14:00 - 15:00
Résumé :
Explaining why the simplex method is fast in practice, despite it taking exponential time in the theoretical worst case, continues to be a challenge. Smoothed analysis is a paradigm for addressing this question. During my talk I will present an improved upper bound on the smoothed complexity of the simplex method, as well as prove the first non-trivial lower bound on the smoothed complexity. This is joint work with Yin Tat Lee and Xinzhi Zhang.
LOVE 01/12/2022 Directed homotopy type theory, par Paige Randall North
Paige Randall North, Utrecht University  
Salle B107, bâtiment B, Université de Villetaneuse
01/12/2022    10:30 - 12:00
Résumé :
In this talk, I will describe the development of a directed homotopy type theory. The aim is to capture (higher) categories and directed topological spaces as models of the theory, and thus use it to study phenomena such as concurrency and rewriting. I will explain homotopy type theory in a way that motivates this generalization, so prior knowledge of homotopy type theory is not required. I will also point out similarities between this work and modal approaches to linear type theory.
COMP 28/11/2022 Machine-Free Complexity 1, par Paulin de Naurois
Paulin de Naurois, CNRS, LIPN  
Hybride (Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
28/11/2022    14:30 - 15:30
Résumé :
LOVE 25/11/2022 Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed Automata, par Laure Petrucci
Laure Petrucci, Équipe LoVe, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
25/11/2022    12:30 - 13:30
Résumé :
We present a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs —e.g., allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies—not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories.
LOVE 25/11/2022 2-dimensional fixpoint operators, par Zeinab Galal
Zeinab Galal, University of Manchester  
Salle B107, bâtiment B, Université de Villetaneuse
25/11/2022    10:30 - 12:00
Résumé :
Fixpoint operators are tools to reason on recursive programs and infinite data types obtained by induction (e.g. lists, trees) or coinduction (e.g. streams). They were given a categorical treatment with the notion of categories with fixpoints. An important result by Plotkin and Simpson in this area states that provided some conditions on bifree algebras are satisfied, we obtain the existence of a unique uniform fixpoint operator. This theorem allows to recover the well-known examples of the category Cppo (complete pointed partial orders and continuous functions) in domain theory and the relational model in linear logic. In this talk, I will present a categorification of this result where the 2-dimensional framework allows to study the coherences associated to the reductions of ?-calculi with fixpoints i.e. the equations satisfied by the program computations steps.
AOC 24/11/2022 Combinatorial solvers and neural networks, par Pasquale Minervini
Pasquale Minervini  
https://bbb.lipn.univ-paris13.fr/b/wol-ma9-vjn - code: 514019
24/11/2022    10:30 - 11:30
Résumé :
Combining discrete probability distributions and combinatorial optimization problems with neural network components has numerous applications but poses several challenges. We propose Implicit Maximum Likelihood Estimation (IMLE), a framework for end-to-end learning of models combining discrete exponential family distributions and differentiable neural components. IMLE is widely applicable as it only requires the ability to compute the most probable states and does not rely on smooth relaxations. The framework encompasses several approaches such as perturbation-based implicit differentiation and recent methods to differentiate through black-box combinatorial solvers. Moreover, we show that IMLE simplifies to maximum likelihood estimation when used in some recently studied learning settings that involve combinatorial solvers. One limitation of IMLE is that, due to the finite difference approximation of the gradients, it can be especially sensitive to the choice of the finite difference step size which needs to be specified by the user. In this presentation, we also introduce Adaptive IMLE (AIMLE), the first adaptive gradient estimator for complex discrete distributions: it adaptively identifies the target distribution for IMLE by trading off the density of gradient information with the degree of bias in the gradient estimates. We empirically evaluate our estimator on synthetic examples, as well as on Learning to Explain, Discrete Variational Auto-Encoders, and Neural Relational Inference tasks. In our experiments, we show that our adaptive gradient estimator can produce faithful estimates while requiring orders of magnitude fewer samples than other gradient estimators.
COMP 21/11/2022 Kolmogorov complexity, par Ulysse Léchine
Ulysse Léchine, LIPN  
Hybride (Salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
21/11/2022    14:30 - 15:30
Résumé :
LOVE 18/11/2022 strategFTO: Untimed control for timed opacity, par Dylan Marinho
Dylan Marinho, Université de Lorraine  
Salle B107, bâtiment B, Université de Villetaneuse
18/11/2022    12:30 - 13:30
Résumé :
We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modeled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, i. e., a set of allowed actions, such that the system restricted to those actions is fully timed-opaque. We first show that this problem is not more complex than the full timed opacity problem, and then we propose an algorithm, implemented and evaluated in practice.
AOC 18/11/2022 On the solution of convex Semi-Infinite Problems, par Martina Cerulli
Martina Cerulli, Essec  
Amphi Copernic
18/11/2022    10:30 - 11:30
Résumé :
In this talk, we will present the results of the paper "Convergent algorithms for a class of convex semi-infinite programs" by M. Cerulli, A. Oustry, C. D'Ambrosio, L. Liberti, accepted for publication on SIAM Journal on Optimization. In this paper, we focus on convex Semi-Infinite Problems (SIPs) with an infinite number of quadratically parametrized constraints, not necessarily convex w.r.t. the parameter. A new convergent approach to solve these SIPs is proposed, leveraging the dualization of the inner problem. Indeed, based on the Lagrangian dual of the inner problem, a convex and tractable restriction of the considered SIP is derived. We state sufficient conditions for the optimality of this restriction. If these conditions are not met, the restriction is enlarged through an Inner-Outer Approximation Algorithm, and its value converges to the value of the original semi-infinite problem. This new algorithmic approach is compared with the classical Cutting Plane algorithm. We propose a new rate of convergence of the Cutting Plane algorithm, directly related to the iteration index, derived when the objective function is strongly convex, and under a strict feasibility assumption. We successfully test the two methods on two applications: the constrained quadratic regression and a zero-sum game with cubic payoff.
LOVE 15/11/2022 An Alternative (Multi-timed) Semantics for Modelling the Behaviour of Distributed Timed Systems, par James Ortiz
James Ortiz, Université de Namur  
Salle B107, bâtiment B, Université de Villetaneuse
15/11/2022    12:15 - 13:30
Résumé :
Distributed Timed Systems ( DTS) can be characterized by several communicating components whose behaviour depends on many timing constraints, and such component can be located at several computers spread over a communication network. Distributed Timed Automata ( DTA) and Timed Automata with Independent Clocks ( icTA) were introduced to model DTS. They are a variant of Timed Automata ( TA) with local clocks that may not run at the same rate. Model checking is a popular technique for automatic formal verification of untimed as well as timed systems. Unfortunately, this technique suffers from the well-known explosion problem: it becomes increasingly difficult to explore exhaustively the whole state space as the system grows, and this problem is exacerbated with the presence of clocks. To handle this problem, many techniques have emerged in recent years, among which bisimulation is popular. Timed bisimulation has already been proven to be decidable for TA. In this talk, I will show our alternative semantics (Multi-timed Automata ( MTA)), which is an extension of TA and icTA, whose execution traces can be modelled as sequences of pairs, where each pair contains an action and a tuple of timestamps. Thus, each action has its own tuple of the local time of occurrence for each component that belongs to the modelling DTS. Then, we have extended the theory of Timed Labelled Transition Systems ( TLTS) to Multi-Timed Labelled Transition Systems ( MLTS) and relate it through our alternative semantics for MTA. Also, we have revisited the notion of timed bisimulation on those automata, resulting in multi-timed bisimulation. We have proved its decidability and presented an EXPTIME algorithm for deciding whether two MTA are multi-timed bisimilar.
COMP 14/11/2022 Barriers in Complexity {II}, par Thomas Seiller
Thomas Seiller, CNRS, LIPN  
Hybrid (room B107 and https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
14/11/2022    14:30 - 15:30
Résumé :
COMP 07/11/2022 A generic proof of the Cook-Levin theorem, par Paulin de Naurois
Paulin de Naurois, LIPN  
Hybride (salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
07/11/2022    14:30 - 16:00
Résumé :
RCLN 07/11/2022 Trustworthy AI: Ethical considerations when using AI techniques, par Fernando Perez-Tellez
Fernando Perez-Tellez, TU Dublin  
Salle B107, bâtiment B, Université de Villetaneuse
07/11/2022    12:30 - 13:30
Résumé :
Recently, Artificial Intelligence (AI) is being used everywhere this is due to the accessibility of this technology in different aspects of everyday life. The idea of incorporating AI systems into several aspects of human life is to benefit humans by reducing labour and increasing everyday conveniences. Independently of the adopted definition of AI, we know that AI can either represent a benefit or an threat (unintentional in most of the cases). Then we should be thinking of creating intelligent systems considering important ethical and legal aspects. Dr. Fernando Perez Tellez, a lecturer and researcher from the Technological University Dublin (TU Dublin), Ireland is visiting LIPN. Dr. Perez Tellez will give a presentation on why is important to consider Ethics when AI techniques are used and how to make responsible use of AI. He will also present his TU Dublin colleagues research interests to promote the creation of potential research collaborations between LIPN and TU Dublin research groups.
COMP 24/10/2022 Algebraic complexity, par Christophe Tollu
Christophe Tollu, LIPN  
Hybride (salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
24/10/2022    14:30 - 15:30
Résumé :
LOVE 24/10/2022 Modular Analysis of Tree-Topology Models, par Jaime Arias
Jaime Arias, Équipe LoVe, LIPN  
BBB : https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
24/10/2022    12:15 - 13:30
Résumé :
Networks of automata that synchronise over shared actions are organised according to a graph synchronisation topology. In this topology, two automata are connected if they can jointly execute some action. We present a very effective reduction for networks with tree-like synchronisation topologies such that all automata after synchronising with their parents can execute only local (non-synchronising) actions: forever or until resetting, i.e. entering the initial state. We show that the reduction preserves reachability, but not liveness. This construction is extended to tree-like topologies of arbitrary automata and investigated experimentally.
COMP 17/10/2022 Boolean circuits, par Damiano Mazza
Damiano Mazza, CNRS, LIPN  
Hybride (salle E303 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
17/10/2022    14:00 - 15:00
Résumé :
As part of the background lectures on complexity theory, this will cover the topic of Boolean circuits.
AOC 13/10/2022 Turn it around. The opportunities of Circular Economy in operation management, par Pablo Andres Maya
Pablo Andres Maya, Universidad de Antioquia Facultad de Medicina: Medellin, Antioquia, CO  
Salle B107, Université de Villetaneuse
13/10/2022    10:30 - 11:30
Résumé :
The traditional economic model based on produce, use, and disposal is reaching its limits. The Circular Economy is an alternative paradigm that envisions a better use of the limited resources we already have. However, putting into practice the circular economy imposes challenges and opportunities to operations management that are still to be addressed. We will discuss the role of analytics and operations research in tackling those challenges.
COMP 10/10/2022 Interactive proofs, par Ulysse Léchine
Ulysse Léchine, LIPN  
Hybride (salle B107 et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy)
10/10/2022    14:30 - 15:30
Résumé :
As part of the background lectures on complexity theory, this will cover the topic of interactive proofs.
COMP 03/10/2022 Barriers in Complexity {I}, par Thomas Seiller
Thomas Seiller, CNRS, LIPN  
Séminaire Hybride: Salle B107 (LIPN) et https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy
03/10/2022    14:30 - 15:30
Résumé :
This is the first of a series of two-to-three lectures on barriers in computational complexity, i.e. negative results showing that (some) proof techniques are inefficient against (some) open problems in the field.
LOVE 15/09/2022 The (infinity,1)-category of Types, par Eric Finster
Eric Finster, University of Birmingham  
Salle B107, bâtiment B, Université de Villetaneuse and online
15/09/2022    10:30 - 11:30
Résumé :
A major outstanding difficulty in Homotopy Type Theory is the description of coherent higher algebraic structures. As an example, we know that the algebraic structure possessed by the collection of types and functions between them is *not* a traditional 1-category, but rather an (infinity,1)-category. In this talk, I will describe how the addition of a finite collection additional definitional equalities designed to render the notion of "opetopic type" definable in fact allows one to construct the (?,1)-category structure on the universe of types.
LOVE 16/06/2022 Parallelism in Soft Linear Logic, par Paulin Jacobé de Naurois
Paulin Jacobé de Naurois, CNRS, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
16/06/2022    10:30 - 11:30
Résumé :
We extend the Soft Linear Logic of Lafont with a new kind of modality, called parallel. Contractions on parallel modalities are only allowed in the cut and the left -o rules, in a controlled, uniformly distributive way. We show that SLL, extended with this parallel modality, is sound and complete for PSPACE. We propose a corresponding typing discipline for the lambda-calculus, extending the STA typing system of Gaboardi and Ronchi, and establish its PSPACE soundness and completeness. The use of the parallel modality in the cut-rule drives a polynomial-time, parallel call-by-value evaluation strategy of the terms.
LOVE 09/06/2022 Bunched Fuzz: Sensitivity for Vector Metrics, par Patrick Baillot
Patrick Baillot, CNRS, Cristal, Lille  
Salle B107, bâtiment B, Université de Villetaneuse
09/06/2022    10:30 - 11:30
Résumé :
"Program sensitivity" measures the distance between the outputs of a program when it is run on two related inputs. This notion, which plays an important role in areas such as differential privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. One approach that has proved particularly fruitful for this domain is the use of type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own notion of distance, and the typing rules explain how those distances can be treated soundly when analyzing the sensitivity of a program. In particular, Fuzz features two products types, corresponding to two different sensitivity analyses: the "tensor product" combines the distances of each component by adding them, while the "with product" takes their maximum. In this talk we will show how products in Fuzz can be generalized to arbitrary Lp distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases L1 and L?. To handle the generalized products, we extend the Fuzz type system with bunches -- as in the logic of bunched implications -- where the distances of different groups of variables can be combined using different Lp distances. We show that our extension, Bunched Fuzz, can be used to reason about important examples of metrics between probability distributions in a natural way. This is joint work with june wunder, Arthur Azevedo de Amorim, and Marco Gaboardi.
AOC 02/06/2022 On two two-level problems for operational warehouse planning in person-to-parts order picking systems, par Stefan Irnich
Stefan Irnich, Gutenberg School of Management and Economics, Chair of Logistics Management - Université de Mainz  
Visio - https://bbb.lipn.univ-paris13.fr/b/wol-ma9-vjn -code 514019
02/06/2022    11:45 - 12:45
Résumé :
We present a new modeling and solution approach for two-level problems in warehousing where one level concerns picking operations in a manual picker-to-parts warehouse. In particular, we consider the single picker routing problem with scattered storage (SPRP-SS) and the joint order batching and picker routing problem (JOBPRP). The SPRP-SS assumes that an article is, in general, stored at more than one pick position. The task is then the simultaneous selection of pick positions for requested articles and the determination of a minimum-length picker tour collecting the articles. In the JOBPRP, a set of orders is given, each with one or several order lines requesting a number of articles. The problem is here to group the given orders into capacity-feasible batches so that the total length of the picker tours collecting the respective articles is minimized. It is a classical result of Ratliff and Rosenthal that, for given pick positions, an optimal picker tour is a shortest path in the state space of a dynamic program with a linear number of states and transitions. We extend the state space of Ratliff and Rosenthal so that every feasible picker tour is still a path. Furthermore, the additional requirement to make consistent selections and grouping decisions can be modeled as additional constraints in shortest-path problems. We propose to solve these problems with a MIP solver. We will explain why this approach is not only convenient and elegant but also generic: it covers optimal solutions to integrated problems that use heuristic routing policies for the picker tours, consider different warehouse layouts, and incorporate further extensions. Computational experiments with a direct MIP solver-based approach for the SPRP-SS and a branch-price-and-cut algorithm for the JOBPRP show that the new modeling and solution approach outperforms the available exact algorithms. The latter computes hundreds of new best and provably optimal solutions to open instances of three JOBPRP benchmark sets. (joint work with Katrin Heßler)
LOVE 19/05/2022 Fully abstract translation for parametric polymorphism to dynamic sealing via game semantics, par Guilhem Jaber
Guilhem Jaber, Université de Nantes  
Salle B107, bâtiment B, Université de Villetaneuse
19/05/2022    10:30 - 11:30
Résumé :
In this talk, we will present trace models for typed higher-order effectful programming languages, including System F, and the cryptographic lambda-calculus, a language with an idealised model of encryption. Our models are defined by representing programs as labeled transition systems generating all possible interactions with the environment, following operational presentation of game semantics. In a setting with mutable store, we provide a proof of full-abstraction, that is equality in the model corresponds to contextual equivalence of the programming language. From these models, we derive a general methodology to build fully-abstract compilation schemes. We apply it to derive the first fully abstract compilation scheme from System F, to the cryptographic lambda-calculus, in presence of mutable store. This compilation scheme can be seen as a refinement of the one proposed by Sumii and Pierce, that was shown to not be fully-abstract by Devriese, Patrignani and Piessens.
LOVE 12/05/2022 Groupoidal Realizability, par Sam Speight
Sam Speight, University of Oxford  
Salle B107, bâtiment B, Université de Villetaneuse
12/05/2022    10:30 - 11:30
Résumé :
I will describe ongoing work attempting to rethink categorical realizability models of type theory in the context of intensional and homotopy type theory. The idea is to equip the Hofmann-Streicher groupoid model of type theory with a notion of realizability analogous to how traditional categories of assemblies do so for the set model. Realizers derive from a "realizer category" that is assumed to have increasingly more structure as we seek to model a more expressive type theory. The key ingredient is an interval qua co-groupoid internal to the realizer category, facilitating a definition of homotopy and an abstract fundamental groupoid construction. Objects in a groupoid are realized by points in some fundamental groupoid; isomorphisms are realized by paths. Insofar as realizability interpretations are said to formalize the (informal) BHK interpretation, we claim that groupoidal realizability formalizes the informal homotopy interpretation of intensional type theory, or the "topological BHK interpretation". I will show how impredicative and univalent universes can be modelled via the relationship between "modest groupoids" and "generalized congruences", and, time permitting, will discuss how this work makes contact with some classical topics in theoretical computer science, such as domain theory and game semantics.
AOC 21/04/2022 Fast algorithms for some parametric optimization problems, par Hassan Aissi
Hassan Aissi, LAMSADE - Paris Dauphine  
Salle B107, bâtiment B, Université de Villetaneuse
21/04/2022    10:30 - 11:30
Résumé :
Parametric optimization is a rich field with applications ranging from sensitivity analysis, Lagrangian relaxation, multiobjective optimization, and minimum-ratio optimization. We consider in this talk some parametric problems related to the minimum cut, in which we are given a graph G=(V,E) with edge costs that are affine functions of a parameter ???d. We develop strongly polynomial algorithms for these problems that are faster than known techniques.
AOC 07/04/2022 Quantum Computing for Process Systems Engineering, par David Bernal Neira
David Bernal Neira, Associate scientist in quantum computing at the Research Institute of Advanced Computer Science (RIACS) of the Universities Space Research Association (USRA) and QuAIL at NASA  
Salle B107, bâtiment B, Université de Villetaneuse
07/04/2022    11:30 - 12:30
Résumé :
Optimization problems arise in different areas of Process Systems Engineering (PSE), and solving these problems efficiently is essential for addressing important industrial applications. Quantum computers have the potential to efficiently solve challenging nonlinear and combinatorial problems. However, available quantum computers cannot solve practical problems; they are limited to small sizes and do not handle constraints well. In this talk, we propose hybrid classical-quantum algorithms to solve mixed-integer nonlinear problems (MINLP) and apply decomposition strategies to break down MINLPs into Quadratic Unconstrained Binary Optimization (QUBO) subproblems that can be solved by quantum computers. We will also cover different approaches to solving Quadratic Unconstrained Binary Optimization (QUBO) problems through unconventional computation methods, including but not limited to Quantum algorithms, and discuss how these approaches lead to algorithms able to outperform classical solution approaches
RCLN 28/03/2022 Abstractive Summarization Evaluation: Overview and Reflections, par Yanzhu Guo
Yanzhu Guo, LIX - Ecole Polytechnique  
Salle B107, bâtiment B, Université de Villetaneuse
28/03/2022    13:00 - 14:30
Résumé :
The topic of summarization evaluation has recently received a surge of attention due to the rapid development of abstractive summarization systems. We conduct a survey of the state-of-the-art evaluation metrics along with relevant datasets and visualization systems. We also touch upon the statistical deficiencies in current meta-evaluation approaches such as the problematic choice of scoring range, the lack of paired evaluation as well as the prevalence of underpowered tests. Finally, we show experimental results proving the unreliability of human-annotated ground-truth reference summaries and thus argue for reference-free metrics as a more promising future direction.
AOC 17/03/2022 A Tailored Benders Decomposition Approach for Last-mile Delivery with Autonomous Robots, par Ivana Ljubic
Ivana Ljubic, ESSEC  
Salle B107, bâtiment B, Université de Villetaneuse
17/03/2022    12:30 - 13:30
Résumé :
This work addresses an operational problem of a logistics service provider that consists of finding an optimal route for a vehicle carrying customer parcels from a central depot to selected facilities, from where autonomous devices like robots are launched to perform last-mile deliveries. The objective is to minimize a tardiness indicator based on the customer delivery deadlines. We provide a better understanding of how three major tardiness indicators can be used to improve the quality of service by minimizing the maximum tardiness, the total tardiness, or the number of late deliveries. We study the problem complexity, devise a unifying Mixed Integer Programming formulation and propose an efficient branch-and-Benders-cut scheme to deal with instances of realistic size. Numerical results show that this novel Benders approach with a tailored combinatorial algorithm for generating Benders cuts largely outperforms all other alternatives. In our managerial study, we vary the number of available facilities, the coverage radius of autonomous robots and their speed, to assess their impact on the quality of service and environmental costs. Joint work with: L. Alfandari and M.M. de Silva
LOVE 11/03/2022 Lightweight (yet efficient) verification of cyber-physical systems, par Étienne André
Étienne André, LORIA  
Salle B107, bâtiment B, Université de Villetaneuse
11/03/2022    11:15 - 12:15
Résumé :
Monitoring of cyber-physical systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals, while real behaviors are continuous-time signals. To mitigate this problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use prior knowledge about the target system to prune interpolation candidates. Technically, we express such prior knowledge by linear hybrid automata (LHAs)---the LHAs are called bounding models. We present two partial algorithms---one is via reduction to reachability in LHAs and the other is a direct one using polyhedra---and show that these methods, and thus the proposed model-bounded monitoring scheme, are efficient and practically relevant. This presentation is based on joint works with Ichiro Hasuo and Masaki Waga.
LOVE 20/01/2022 Functional interpretations and applications, par [Chocola] Bruno Dinis
[Chocola] Bruno Dinis, Universidade de Lisboa, Portugal  
https://chocola.ens-lyon.fr/events/meeting-2022-01-20/
20/01/2022    10:00 - 12:00
Résumé :
Functional interpretations are maps of formulas from the language of one theory into the language of another theory, in such a way that provability is preserved. These interpretations typically replace logical relations by functional relations. Functional interpretations have many uses, such as relative consistency results, conservation results, and extraction of computational content from proofs as is the case in the so-called proof mining program. I will present several recent functional interpretations and some results that come from these interpretations. I will also give examples of application of functional interpretations, in the spirit of the proof mining program.
LOVE 13/01/2022 Extended Addressing Machines for PCF, with Explicit Substitutions, par Nicolas Munnich
Nicolas Munnich, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse (retransmis sur BBB: https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983))
13/01/2022    10:30 - 11:30
Résumé :
Addressing machines have been introduced as a formalism to construct models of the pure, untyped lambda-calculus. We extend the syntax of their programs by adding instructions for executing arithmetic operations on natural numbers, and introduce a reflection principle allowing certain machines to access their own address and perform recursive calls. We prove that the resulting extended addressing machines naturally model a weak call-by-name PCF with explicit substitutions. Finally, we show that they are also well suited for representing regular PCF programs (closed terms) computing natural numbers.
LOVE 06/01/2022 Bayesian Networks and Proof-Nets, par Claudia Faggian
Claudia Faggian, IRIF, CNRS & Université de Paris  
En ligne: https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
06/01/2022    10:30 - 11:30
Résumé :
(Joint work with Thomas Ehrhard and Michele Pagani) Bayesian networks are a powerful tool for probabilistic reasoning. They allow for a compact representation of large probability distributions, and for efficient inference algorithms. A Bayesian Network consists of two parts: a qualitative component in the form of a directed acyclic graph (DAG), and a quantitative component, in the form conditional probabilities. Strikingly, linear logic proof-nets have a similar nature: a graph structure represents the proof, a quantitative interpretation yields the semantics. In this talk, we present recent (and on-going) work to explore the connection between Bayesian Networks and (Multiplicative) Proof-Nets, uncovering a strong correspondence between the two structures, and their quantitative interpretation.
LOVE 09/12/2021 Refining vector spaces using norms, par Nicolas Blanco
Nicolas Blanco, University of Birmingham  
Salle B107, bâtiment B, Université de Villetaneuse (retransmis sur BBB)
09/12/2021    10:30 - 11:30
Résumé :
In this talk, I will introduce the theory of bifibrations of polycategories and its relation to refinement types and classical multiplicative linear logic. I will illustrate this on an example, where norms are seen as refining vector spaces. I will explain how to recover the norms for interpreting the connectives of MLL using this perspective. I will also show how it shed light on some other properties of these norms. I will conclude by mentioning some possible extensions of this work.
LOVE 02/12/2021 Journée-Séminaire Chocola
 
ENS Lyon
02/12/2021    09:30 - 17:00
Résumé :
LOVE 29/11/2021 Guaranteed properties of dynamical systems under perturbations, par Jawher Jerray
Jawher Jerray, LIPN, Équipe LoVe  
Salle B107, bâtiment B, Université de Villetaneuse
29/11/2021    12:00 - 13:00
Résumé :
ince dynamical systems has a major impact on human development, especially critical systems that can put human lives at risk if something goes wrong. Hence, the need of studying the behavior of these systems in order to guarantee their correct functioning. Nevertheless, computing such type of system has never been an easy task, as the complexity of these systems is constantly increasing, in addition to the perturbations that may arise during their performance, as well as undefined parameters that may exist. To ensure that a system always produces the expected results and does not fail in any way, a formal verification of its behavior and properties is necessary. In this work, we study dynamical systems from different aspects and using various techniques. More specifically, we focus on the formal verification of some of its critical properties such as schedulability, synchronization, robustness and stability. In the first part, we study the schedulability of the flight control of a space launcher with unknown parameters and under constraints. Then, we propose a synthesis of the admissible timing values of the unknown parameters by a parametric timed model checker. We increase the complexity of the problem by taking into consideration the switch time between two threads. We extend this work by developing a tool that translates a given real-time system design into parametric timed automata in order to infer some timing constraints ensuring schedulability. In the second part, we study the stability of dynamical systems and the robustness of controls. We give a simple technique based on Euler's integration method which allows to build an invariant set around a given system. This technique guarantees that the approximate Euler solutions are attracted by a limit cycle. We apply the method on different systems, including chaotic systems with strange attractors. Furthermore, we show that a basic combination of a random sampling with a symbolic computation method assists to deal with robust control problems for nonlinear systems. Also, we illustrate a basic condition guaranteeing that a system with perturbation is robust under a repeated control sequence obtained by solving a horizon optimal control problem. Finally, we unified the main contributions of the second part in a tool called ORBITADOR which checks the stability of a given system and notably returns plots containing the evolution of the system in different views and the shape of the invariant if it exists.
LOVE 29/11/2021 A General Framework for Supervision of Opacity, par Nour SOUID
Nour SOUID, LIPN, Équipe LoVe  
Salle B107, bâtiment B, Université de Villetaneuse
29/11/2021    11:00 - 12:00
Résumé :
Opacity is a property of information flow that characterizes the ability of a system to keep an information secret from a third party called an attacker. In this paper, we investigate the problem of reinforcing the opacity using the Supervisory Control Theory. We present a novel approach to synthesize a supervisor to the system that prevents, at run time, a malicious observer from deducing secret information. Our approach is general since it does not take into consideration the relationship between the attacker's observation and the supervisor's one. Moreover, being based on formal methods, it allows us to represent various systems in different contexts. Particularly, we focus on web services and we apply our approach to a B2B (business-to-business) e-commerce use case.
AOC 25/11/2021 SMS++: a Structured Modelling System with ... hopefully, one day ... some useful application?, par Antonio Frangioni
Antonio Frangioni, Università di Pisa  
Salle B107, bâtiment B, Université de Villetaneuse
25/11/2021    10:30 - 11:30
Résumé :
On February this year, after about 8 years of gestation, an early beta release of the Structured Modelling System++ has been released to general public availability. SMS++ is a C++ library intended to facilitate the development of very large optimization problems with multiple nested heterogeneous structure, and especially of the corresponding solution methods, chiefly (but not exclusively) ones based on (parallel) decomposition. In the attempt of achieving this goal SMS++ has accrued a number of features that look quite unique in the landscape of modelling systems, so much so as to raise the legitimate suspicion that the reason why these features have never been developed before is because no sane person would have ever thought them a good idea. Yet the system is there and it does seem to offer some new viewpoints on mathematical modelling systems that may at least be worth a look. SMS++ is itself developed in an highly modular fashion and already counts a(n hopefully growing) number of separate sub-projects besides the "core" library and the support tools. One of these allows to solve Lagrangian Duals of complex integer programs with remarkable ease, and it will hopefully soon be joined by a similar component doing Benders' decomposition. Hence, there may actually be a few use cases in which SMS++ could be worth considering already, despite the very many missing components that would be needed to make it a really compelling prposition. In fact, perhaps the most interesting feature of SMS++ is it being community-oriented and (at least in principle) almost infinitely extendable to try to cater for the very diverse needs of the disparate clades of the optimization world. This alone may make it worth a second look, notwithstanding the arguably insane delusions of an all-conquering modelling system that some of the developers harbour and that would require capturing an unfeasibly large amount of mindshare to achieve.
LOVE 25/11/2021 Superpolynomial Lower Bounds Against Low-Depth Algebraic Circuits, par Nutan Limaye, Srikanth Srinivasan, Sebastien Tavenas
Nutan Limaye, Srikanth Srinivasan, Sebastien Tavenas, ITU Copenhagen, Aarhus University, CNRS & Université Savoie-Mont-Blanc  
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
25/11/2021    10:00 - 11:00
Résumé :
An Algebraic Circuit for a polynomial PF[x1xN] is a computational model for constructing the polynomial P using only additions and multiplications. It is a syntactic model of computation, as opposed to the Boolean Circuit model, and hence lower bounds for this model are widely expected to be easier to prove than lower bounds for Boolean circuits. Despite this, we do not have superpolynomial lower bounds against general algebraic circuits of depth 3 (except over constant-sized finite fields) and depth 4 (over fields other than F2), while constant-depth Boolean circuit lower bounds have been known since the early 1980s. In this paper, we prove the first superpolynomial lower bounds against general algebraic circuits of all constant depths over all fields of characteristic 0 (or large). We also prove the first lower bounds against homogeneous algebraic circuits of constant depth over any field. Our approach is surprisingly simple. We first prove superpolynomial lower bounds for constant-depth Set-Multilinear circuits. While strong lower bounds were already known against such circuits, most previous lower bounds were of the form f(d)poly(N), where d denotes the degree of the polynomial. In analogy with Parameterized complexity, we call this an FPT lower bound. We extend a well-known technique of Nisan and Wigderson (FOCS 1995) to prove non-FPT lower bounds against constant-depth set-multilinear circuits computing the Iterated Matrix Multiplication polynomial IMMnd (which computes a fixed entry of the product of d nn matrices). More precisely, we prove that any set-multilinear circuit of depth computing IMMnd must have size at least ndexp(?O()) This result holds over any field, as long as d=o(logn). We then show how to convert any constant-depth algebraic circuit of size s to a constant-depth set-multilinear circuit with a blow-up in size that is exponential in d but only polynomial in s over fields of characteristic 0. (For depths greater than 3, previous results of this form increased the depth of the resulting circuit to (logs).) This implies our constant-depth circuit lower bounds. We can also use these lower bounds to prove a Depth Hierarchy theorem for constant depth circuits. We show that for every depth , there is an explicit polynomial which can be computed by a depth circuit of size s, but requires circuits of size s(1) if the depth is ?1. Finally, we observe that our superpolynomial lower bound for constant-depth circuits implies the first deterministic sub-exponential time algorithm for solving the Polynomial Identity Testing (PIT) problem for all small depth circuits using the known connection between algebraic hardness and randomness.
LOVE 22/11/2021 Can a single transition stop an entire Petri net?, par Prof. Dr. Jörg Desel
Prof. Dr. Jörg Desel, FernUniversität in Hagen  
Salle B107, bâtiment B, Université de Villetaneuse
22/11/2021    13:00 - 14:00
Résumé :
A transition stops a Petri net if, from any reachable marking, each occurrence sequence without this transition is finite. For bounded Petri nets it is easy to decide if a transition stops a net. We show that the coverability graph can be used to decide the property for unbounded Petri nets. A corresponding tool considers moreover generalisations of the above property.
LOVE 18/11/2021 Implementing the mwp-flow analysis, par Neea Rusch
Neea Rusch, University of Augusta  
Salle B107, bâtiment B, Université de Villetaneuse (retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24; code d'accès 749983)
18/11/2021    10:30 - 11:30
Résumé :
Jones and Kristiansen’s mwp-flow analysis certifies polynomial bounds on the size of the values returned by an imperative program. This method is compositional, extensible and elegant, as it bounds transitions between states instead of focusing on states in isolation. While simple to use, this theoretical result is difficult to prove correct and implement. Here we detail the challenges a naive implementation has to face, and how we remedied them to offer a fast, efficient and extended implementation of the technique. The result, pymwp, is a lightweight tool to automatically perform data-size analysis of C programs. This effort prepares and enables the development of certified complexity analysis, by transforming a costly analysis into a tractable program, that leverages compositionality and decorrelates the problem of finding the existence of a bound with its value.
AOC 18/11/2021 Optimization + Simulation: how to reduce bus bunching, par Yasmin A Rios Solis
Yasmin A Rios Solis, Escuela de Ingeniería y Ciencias - Campus Monterrey - Tecnológico de Monterrey, México  
ATTENTION Salle D215, bâtiment D, Université de Villetaneuse
18/11/2021    10:30 - 11:30
Résumé :
Real-time control strategies palliate with the day's dynamics in bus rapid transit systems. In this talk, we focus on a bus bunching problem that minimizes the number of buses of the same line cruising head-to-tail or arriving at a stop simultaneously by using bus holding times at the stops. For this, we propose a new mathematical model with quadratic constraints, whose objective function minimizes the penalties caused by buses that are bunching. Experimental results on a simulation of a bus rapid transit system in Monterrey, Mexico, show the efficiency of our approach. The results show a bus bunching reduction of 45% compared to the case without optimization. Moreover, in some scenarios the passenger waiting times are reduced by 30%.
LOVE 15/11/2021 Model Checking of Solidity Smart Contracts Adopted For Business Processes, par Ikram Garfatta
Ikram Garfatta, LIPN, Équipe LoVe  
Salle B107, bâtiment B, Université de Villetaneuse
15/11/2021    14:00 - 15:00
Résumé :
Several features of the Blockchain technology are well aligned with critical issues in the Business Process Management (BPM) field, and yet adopting Blockchain for BPM should not be taken lightly. In fact, the security of smart contracts, which are one of the main elements of the Blockchain that make the integration with BPM possible, has proved to be vulnerable. It is therefore crucial for the protection of the designed business processes to prove the correctness of the smart contracts to be deployed on a blockchain. In this talk, I will present our formal approach based on the transformation of Solidity smart contracts, with consideration of the BPM context in which they are used, into a Hierarchical Coloured Petri net. We express a set of smart contract vulnerabilities as temporal logic formulae and use the Helena model checker to, not only detect such vulnerabilities while discerning their exploitability, but also check other temporal-based contract-specific properties.
LOVE 15/11/2021 A Smart Software System for Fire Risk Notification, par Prof. Lars Michael Kristensen
Prof. Lars Michael Kristensen, Software Engineering Research Group - Western Norway University of Applied Sciences  
Salle B107, bâtiment B, Université de Villetaneuse
15/11/2021    13:00 - 14:00
Résumé :
Cold winter seasons result in very dry indoor conditions and have historically led to severe fires in the high and dense representation of wooden homes in Norway. To reduce fire conflagration probability and consequences, it is necessary to have an accurate estimate of the current and near future fire risk to take proper planning precautions. The DYNAMIC research project supported by the Norwegian Research Council has two main objectives: 1) to develop (mathematical) fire risk models that are able to quantify fire risk; 2) to investigate how cloud computing services providing access to weather data can be combined with recent developments in fire risk modelling to enable smart and fine-grained fire risk prediction services. The first part of the talk presents results from a first prototype implementation of a microservice-based fire risk notification system that has been experimentally validated at selected geographical locations in Norway. The system relies on weather data provided by cloud services of the Norwegian Meteorological Institute. Our experimental evaluation demonstrates the ability to provide trustworthy and accurate fire risk indications using a combination of recorded weather data and forecasts. Furthermore, our cloud- and micro-service software system implementation is efficient with respect to data storage and computation time. The second part of the talk presents work-in-progress on formal modelling and behavioural validation of the software architecture for the fire risk notification system.
RCLN 12/11/2021 Relation Extraction with Distant Supervision: noise Reductio, par Juan Luis Garcia-Mendoza
Juan Luis Garcia-Mendoza, Laboratorio de Tecnologias del Lenguaje, INAOE Puebla  
Salle B107, bâtiment B, Université de Villetaneuse
12/11/2021    12:30 - 13:45
Résumé :
Distant Supervision is an approach that allows automatic labeling of instances. This approach has been used in Relation Extraction. Still, the main challenge of this task is handling instances with noisy labels (e.g., when two entities in a sentence are automatically labeled with an invalid relation). The approaches reported in the literature addressed this problem by employing noise-tolerant classifiers. However, if a noise reduction stage is introduced before the classification step, this increases the macro precision values or keep the same values with fewer instances. An approach based on Adversarial Autoencoders is proposed to obtain a new representation that allows noise reduction in Distant Supervision.
LOVE 28/10/2021 Variable binding and substitution for (nameless) dummies, par Ambroise Lafont
Ambroise Lafont, University of Sydney  
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
28/10/2021    10:30 - 11:30
Résumé :
By abstracting over well-known properties of De Bruijn's representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi's approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms. Joint work with Tom & Andre Hirschowitz, Marco Maggesi
LOVE 21/10/2021 [Séminaire Chocola] Program verification on a capability machine in the presence of untrusted code, par Armaël Guéneau
Armaël Guéneau, University of Aarhus  
https://chocola.ens-lyon.fr/events/online-2021-10-22/
21/10/2021    10:00 - 12:00
Résumé :
A capability machine is a kind of CPU with hardware support for fine-grained privilege separation. Practical designs and prototypes for such machines are seeing recent development as part of the CHERI project (University of Cambridge, SRI, ARM) (cheri-cpu.org, morello-project.org), making capability machines a promising target for designing and building new software with security in mind. In this talk, I will present some of the work done at Aarhus University and KU Leuven on developing formal principles for reasoning about security properties of code running on capability machines. I will show how one can prove functional correctness of programs that interact with untrusted (and possibly malicious) code while leveraging capabilities to protect their private state. The key aspects of this methodology are a program logic for reasoning about known code, and a logical relation providing a /universal contract/ of unknown code. The whole work has been mechanized in Coq using the Iris framework.
AOC 14/10/2021 Incorporating Holding Costs in Continuous-Time Service Network Design: New Model, Relaxation and Exact Algorithm, par Roberto Baldacci
Roberto Baldacci, Department of Electrical, Electronic, and Information Engineering “Guglielmo Marconi”, University of Bologna, Italy  
ATTENTION : Salle C311, bâtiment C, Université de Villetaneuse
14/10/2021    10:30 - 11:30
Résumé :
The continuous-time service network design problem (CTSNDP) occurs widely in practice. It aims to minimize the total operational cost by optimizing schedules of transportation services and routes of shipments for dispatching, which can occur at any time point along a continuous planning horizon. In order to be cost effective, shipments often wait to be consolidated, which incurs holding cost. Despite its importance, the holding cost has not been taken into account in the existing studies on the CTSNDP, since introducing it will significantly complicate the problem and make the solution development very challenging. To tackle this challenge, we develop a new dynamic discretization discovery algorithm, which can solve the CTSNDP with holding cost to exact optimum. The algorithm is based on a novel relaxation model and several new optimization techniques. Results from extensive computational experiments validate the efficiency and effectiveness of the new algorithm, as well as demonstrating the benefits that can be gained by taking into account holding costs in solving the CTSNDP. In particular, we show that the significance of the benefits depends on the connectivity of the underline physical network and the flexibility of the shipments’ time requirements.
LOVE 14/10/2021 Logique(s) linéaire(s) indexée(s) : syntaxe, structure et sémantique du fragment multiplicatif-additif, par Flavien Breuvart
Flavien Breuvart, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
14/10/2021    10:30 - 11:30
Résumé :
Nous allons décrire la logique linéaire indexée introduite par T.Ehrhard et A.Bucciarelli il y a 20 ans, expliquer en quoi cette logique est à la fois similaire à d'autres mais avec des particularités uniques. En particuliers nous verrons ses liens avec les logiques BLL-like avec aussi des exponentielles indexées. Dans un troisième temps nous expliquerons comment généraliser l'un et l'autre pour y greffer une notion abstraite de structure de ressources. Enfin, et selon les désir de l’audience, nous allons traiter l'aspect sémantique (catégorique et/or dénotationnel) du fragment additif de ces généralisation.
LOVE 30/09/2021 Call-by-Value, Again!, par Axel Kerinec
Axel Kerinec, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
30/09/2021    10:30 - 11:30
Résumé :
The quest for a fully abstract model of the call-by-value ?-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. In this presentation we study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many ?-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus – especially solvability. We also prove the decidability of the inhabitation problem for our type system. This is joint work with Simona Ronchi Della Rocca and Giulio Manzonetto, published at FSCD 2021.
AOC 23/09/2021 Design of diversified package tours for the digital travel industry : A branch-cut-and-price approach , par Laurent Alfandari
Laurent Alfandari, ESSEC  
Salle B107, bâtiment B, Université de Villetaneuse
23/09/2021    10:30 - 11:30
Résumé :
Motivated by the revolution brought by the internet and communication technology in daily life, this paper examines how the online travel agencies (OTA) can use these technologies to improve customer value. We consider the design of a fixed number of package tours offered to customers in the digital travel industry. This can be formulated as a Team Orienteering Problem (TOP) with restrictions on budget and time. Different from the classical TOP, our work is the first one to introduce controlled diversity between tours. This enables the OTA to offer tourists a diversified portfolio of tour packages for a given period of time, each potential customer choosing a single tour in the selected set, rather than multiple independent tours over several periods as in the classical TOP. Tuning the similarity parameter between tours enables to manage the trade-off between individual preferences in consumers’ choices and economies of scale in agencies’ bargaining power. We propose compact and extended formulations and solve the master problem by a branch-and-price method, and an alternative branch-cut-and-price method. The latter uses a delayed dominance rule in the shortest path pricing problem solved by dynamic programming. A particularity of the model is that in the column generation phase, the diversity constraints hold between each pair of columns, which is unusual and requires to generate these constraints on the fly. Our methods are tested over benchmark TOP instances of the literature, and a real dataset collected from a Chinese OTA. We explore the impact of tours diversity on all stakeholders, and assess the computational performance of the various approaches.
LOVE 16/09/2021 Physic-agnostic computational models, par Titouan Carette
Titouan Carette, LORIA & LRI  
Salle B107, bâtiment B, Université de Villetaneuse -- retransmis sur https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès 749983)
16/09/2021    10:30 - 11:30
Résumé :
Here is a (not so...) secret recipe to write a lot of papers: take any computational concept you like and add quantum, probabilistic, reversible, etc... before the name. In practice this is however not so easy, it often requires to start from scratch to find a formulation fitting our specific framework. Another way is to formulate the computational concept in an abstract language that can then be instantiated to the physical theory we have in mind. This can be done using category theory. An abstract computational process is represented by a string diagram and then interpretation functors provide semantics in various physical models. In this talk I will provide an example of such physic-agnostic model in the form of a diagrammatic approach to quantum streams. We will see that once we have designed the abstract graphical model, varying the physical theory can lead to interesting computational but also physical considerations.
LOVE 01/07/2021 [Séminaire Chocola] Milner and Alur walk into a bar, par Daniele Varacca
Daniele Varacca, LACL - Univ Paris Est Creteil  
https://chocola.ens-lyon.fr/events/online-2021-07-01/
01/07/2021    10:00 - 12:00
Résumé :
The chef kicks them out: "I'm sorry, in my kitchen we only use induction". This talk will start from Morris' PhD thesis in 1968 and present 50 years of theoretical computer science, through PCF, CCS, Alternating transition systems, contexts and strategies, ending up at the footsteps of the monumental Palace of Justice in Créteil.
LOVE 29/06/2021 Fault-tolerant LU factorization is low cost, par Daniel Torres Gonzalez
Daniel Torres Gonzalez, LIPN  
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
29/06/2021    15:00 - 16:00
Résumé :
At large scale, failures are statistically frequent and need to be taken into account. Tolerating failures has arisen as a major challenge in parallel computing as the size of the systems grow, failures become more common and some computation units are expected to fail during the execution of a program. Algorithms used in these programs must be scalable, while being resilient to hardware failures that will happen during the execution. In this presentation, we present an algorithm that takes advantage of intrinsic properties of the scalable communication-avoiding LU algorithms in order to make them fault-tolerant and proceed with the computation in spite of failures. We evaluate the overhead of the fault tolerance mechanisms with respect to failure-free execution on both tall- and-skinny matrices (TSLU) and square matrices (CALU), and the cost of a failure during the execution.
LOVE 17/06/2021 [Séminaire Chocola] Focused nested calculi applied to the logic of bunched implications, par Sonia Marin
Sonia Marin, University College London  
https://chocola.ens-lyon.fr/events/online-2021-06-17/talks/marin/
17/06/2021    10:00 - 12:00
Résumé :
Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics. With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness. Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.
LOVE 03/06/2021 [Séminaire Chocola] Internalizing Representation Independence with Univalence, par Carlo Angiuli
Carlo Angiuli, Carnegie Mellon University  
https://chocola.ens-lyon.fr/events/online-2021-06-03/talks/angiuli/
03/06/2021    15:00 - 17:00
Résumé :
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. In the dependently-typed setting, however, we would like to appeal to such invariance results within a language itself, in order to transfer theorems from simple to complex implementations. Homotopy type theorists have noted that Voevodsky's univalence principle equates isomorphic structures, but unfortunately many instances of representation independence are not isomorphisms. In this talk, we describe a technique for establishing internal relational representation independence results in Cubical Agda by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at https://dl.acm.org/doi/10.1145/3434293.
RCLN 31/05/2021 Knowledge-based Detection of Automatically Generated Text, par Vijini Liyanage
Vijini Liyanage, LIPN  
Salle A303, Bâtiment A, LIPN
31/05/2021    13:00 - 14:00
Résumé :
Séminaire de Vijini Liyanage, étudiante du groupe RCLN, qui va nous présenter son sujet de thèse et les premières étapes de sa thèse sur la détection des textes générés automatiquement par des modèles de langage neuronales, du genre GPT-2.
AOC 20/05/2021 Decomposition methods and column/matrix generation approaches for quadratic programming, par Lucas Létocart
Lucas Létocart, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
20/05/2021    10:30 - 11:30
Résumé :
The purpose of this talk is to present three decomposition approaches for quadratic problems. First, we analyze a simplicial decomposition like algorithmic framework that handles convex quadratic programs in an effective way. We also propose a branch & bound approach based on this simplicial decomposition for the binary case and we introduce warmstart techniques using columns' projection. Then, we propose a methodological analysis on a family of reformulations combining Dantzig-Wolfe decomposition and Quadratic Convex Reformulation principles for binary quadratic problems. Finally, we propose a matrix generation method for quadratically constrained 0-1 quadratic problems based on a Dantzig-Wolfe reformulation. The domain of this relaxation corresponds to the Boolean Quadric Polytope.
LOVE 20/05/2021 [Séminaire Chocola] Monads, equational theories, and metrics for nondeterministic and probabilistic systems, par Valeria Vignudelli
Valeria Vignudelli, ENS Lyon  
https://chocola.ens-lyon.fr/events/online-2021-05-20/
20/05/2021    10:00 - 12:00
Résumé :
Monads and their presentations via equational theories provide a tool for reasoning about programs with computational effects. In recent works, we have studied monads resulting from the combination of nondeterminism, probabilities, and termination, as well as their extensions to the category of metric spaces. In this talk, we'll introduce this framework and show applications to proving equivalences and distances of nondeterministic and probabilistic systems. Bibliography: Bonchi, Sokolova, Vignudelli. The theory of traces for systems with nondeterminism and probabilities. LICS 2019. Available at: https://arxiv.org/abs/1808.00923 Mio, Vignudelli. Monads and quantitative equational theories for nondeterminism and probabilities. CONCUR 2020. Available at: https://arxiv.org/abs/2005.07509 Mio, Sarkis, Vignudelli. Combining nondeterminism, probability, and termination: equational and metric reasoning. LICS 2021. Available at: https://arxiv.org/abs/2012.00382
LOVE 06/05/2021 [Séminaire Chocola] Fixpoint Theory -- Upside Down, par Barbara König
Barbara König, Universität Duisburg-Essen  
https://chocola.ens-lyon.fr/events/online-2021-05-06/
06/05/2021    10:00 - 12:00
Résumé :
Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotone function over a complete lattice as the largest post-fixpoint, naturally leads to the so-called coinduction proof principle for showing that some element is below the greatest fixpoint (e.g., for providing bisimilarity witnesses). The dual principle, used for showing that an element is above the least fixpoint, is related to inductive invariants. This talks considers proof rules which are similar in spirit but for showing that an element is above the greatest fixpoint or, dually, below the least fixpoint. The theory is developed for non-expansive monotone functions on suitable lattices of the form M^Y, where Y is a finite set and M an MV-algebra, and it is based on the construction of (finitary) approximations of the original functions. We show that our theory applies to a wide range of examples, including termination probabilities, behavioural distances for probabilistic automata and bisimilarity. Moreover it allows us to determine original algorithms for solving simple stochastic games.
AOC 22/04/2021 Extraction et partitionnement pour la recherche de régularités : application à l'analyse de dialogues., par Zacharie ALES
Zacharie ALES, ENSTA Paris | Institut Polytechnique de Paris  
Salle B107, bâtiment B, Université de Villetaneuse
22/04/2021    10:30 - 11:30
Résumé :
Dans le cadre de l'aide à l'analyse de dialogues, un corpus de dialogues peut être représenté par un ensemble de tableaux d'annotations encodant les différents énoncés des dialogues. Afin d'identifier des schémas dialogiques mis en œuvre fréquemment, nous définissons une méthodologie en deux étapes : extraction de motifs récurrents, puis partitionnement de ces motifs en classes homogènes constituant des régularités. Deux méthodes sont développées afin de réaliser l'extraction de motifs récurrents : LPCA-DC et SABRE. La première est une adaptation d'un algorithme de programmation dynamique tandis que la seconde est issue d'une modélisation formelle du problème d'extraction d'alignements locaux dans un couple de tableaux d'annotations. Le partitionnement de motifs récurrents est réalisé par deux formulations originales du problème de K-partitionnement sous la forme de programmes linéaires en nombres entiers. Lors d'une étude polyèdrale, nous caractérisons des facettes d'un polyèdre associé à ces formulations (notamment les inégalités de 2-partitions, les inégalités 2-chorded cycles et les inégalités de clique généralisées). Ces résultats théoriques permettent la mise en place d'un algorithme de plans coupants résolvant efficacement le problème. Nous développons le logiciel d'aide à la décision VIESA, mettant en œuvre ces différentes méthodes et permettant leur évaluation au cours de deux expérimentations réalisées par un expert psychologue. Des régularités correspondant à des stratégies dialogiques que des extractions manuelles n'avaient pas permis d'obtenir sont ainsi identifiées.
LOVE 22/04/2021 [Séminaire Chocola] The Time and Space of Interaction, par Gabriele Vanoni
Gabriele Vanoni, Università di Bologna  
https://chocola.ens-lyon.fr/events/online-2021-04-22/
22/04/2021    10:00 - 12:00
Résumé :
Girard's Geometry of Interaction (GOI) can be made concrete by considering it as an implementation technique for functional programs, in particular the lambda calculus. Our work is about the complexity analysis of the abstract machine based on the GOI, the interaction abstract machine (IAM). We have adapted in a non trivial way de Carvalho's non idempotent intersection types so that type derivations completely characterize the time and space complexity of the IAM, thus providing a logical account of the IAM resource usage. Moreover, by the way of the type systems we have introduced, we are able to state some negative results about time and space cost models for the lambda calculus based on the IAM. This is joint work with Beniamino Accattoli and Ugo Dal Lago.
AOC 15/04/2021 Formulations PLNE pour un problème d'ordonnancement juste-à-temps, par Anne-Elisabeth FALQ
Anne-Elisabeth FALQ, Sorbonne université, CNRS, LIP6, équipe RO  
Salle B107, bâtiment B, Université de Villetaneuse
15/04/2021    10:30 - 11:30
Résumé :
Une contrainte essentielle pour un problème d'ordonnancement sur une machine est le non-chevauchement des tâches: deux tâches ne peuvent être exécutées en même temps. Les premières inégalités de non-chevauchement ont été proposées par Queyranne (1993) pour le problème de minimisation de la somme pondérée des dates de fins. La famille d'inégalités linéaires proposée décrit exactement l'enveloppe convexe des vecteurs encodant des ordonnancements réalisables par les dates de fins des tâches. Ces inégalités ne coupent pas tous les vecteurs encodant un ordonnancement avec chevauchement mais assurent le non-chevauchement au sens où tous les points extrêmes du polyèdre qu'elles définissent encodent des ordonnancements réalisables, et plus précisément ceux calés à gauche qui forment un ensemble dominant pour ce problème. Dans cet exposé, nous nous intéresseront particulièrement au problème d'ordonnancement juste-à-temps où toutes les tâches partagent une même date d'échéance commune et où il s'agit de minimiser la somme pondérée des avances et des retards par rapport à cette date. En s'appuyant sur les propriétés de dominance connues pour ce problème NP-difficile (Hall et Posner, 1991), nous proposerons une formulation basée sur des inégalités de non-chevauchement nouvelles. Cette formulation, qui n'est pas exactement un programme linéaire en nombre entiers (PLNE) puisqu'elle fait apparaître des contraintes d'extremalité, peut être résolue par un solveur de PL implémentant un algorithme de "Branch-and-Cut". Nous expliquerons comment et présenterons quelques résultats expérimentaux. Dans un second temps, nous proposerons une formulation compacte pour ce problème, que nous renforçons par des inégalités dites de dominance. Ces inégalités sont ainsi nommées car elles traduisent la dominance des solutions localement optimales, où local s'entend pour un voisinage généré par une famille d'opérations sur les solutions. Pour chaque opération considérée, une inégalité élimine les solutions qu'on pourrait améliorer en appliquant la transformation. De ce fait, ces inégalités coupent des point entiers, et diffèrent en cela des inégalités classiques de renforcement. Grâce à des résultats expérimentaux, nous montrerons le gain d’efficacité qu'apporte ces inégalités de dominance.
LOVE 15/04/2021 Categorifying Non-Idempotent Intersection Types, 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é :
Non-idempotent intersection types can be seen as a syntactic presentation of a well-known denotational semantics for the lambda-calculus, the category of sets and relations. Building on previous work, we present a categorification of this line of thought in the framework of bang calculus, an untyped version of Levy's call-by-push-value. We define a bicategorical model for the bang calculus, whose syntactic counterpart is a suitable category of types. In the framework of distributors, we introduce intersection type distributors, a bicategorical proof relevant refinement of relational semantics. Finally, we prove that intersection type distributors characterize normalization at depth 0. This is joint work with Federico Olimpieri, published at CSL 2021.
LOVE 08/04/2021 [Séminaire Chocola] Sketching type theories, par Daniel Gratzer
Daniel Gratzer, Aarhus University  
https://chocola.ens-lyon.fr/events/online-2021-03-25/
08/04/2021    10:00 - 12:00
Résumé :
Recent developments in type theory have attempted to systematically recast properties of the syntax of a type theories (canonicity, normalization, etc.) into equivalent questions about the category of models. This dictionary relies on a formal link between the syntax of a theory and its category of models: the syntax of the theory must organize into an initial model. To expedite this process, several logical frameworks have been proposed which provide schemata for defining a type theory so that it automatically determines a category of models in which syntax is initial. In this talk, rather than giving a new logical framework per se, we propose a new discipline for creating logical frameworks based around finitary 2-monads and sketches. As a case study of this approach, we show how locally Cartesian closed categories provide a suitable doctrine for type theories. We illustrate how a general theory of sketches [KPT99] can be used to define syntactic categories for type theories in a style that resembles the use of Martin-Löf's Logical Framework [NPS90], following the "judgments as types" principle [HHP93, ML87]. We prove a semantic adequacy result for locally Cartesian closed categories relative to Uemura's representable map categories [Uem19]: if a theory is definable in the framework of Uemura, the locally Cartesian closed category that it generates is a conservative (fully faithful) extension of its syntactic representable map category. On this basis, we argue for the use of locally Cartesian closed categories as a simpler alternative to Uemura's representable map categories. This is joint work with Jonathan Sterling, and a preprint is available on arxiv: https://arxiv.org/abs/2012.10783
LOVE 07/04/2021 Approche formelle pour la vérification formelle de la composition de logiciels, par Mohamed Graiet
Mohamed Graiet  
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
07/04/2021    09:00 - 10:00
Résumé :
La réutilisation est un concept clé dans la construction de systèmes logiciels. Elle permet de composer un ensemble de logiciels existants pour construire de nouveaux logiciels à valeur ajoutée. Dans le contexte de notre travail, on s'intéresse à la composition de deux types de logiciels, à savoir les services Web et logiciels libres à base de packages FOSS (Free and Open Source Software). La vérification de la correction de la composition pour la sécurité de logiciels FOSS et de services Web reste l’une des tâches les plus difficiles malgré les efforts et les travaux de recherches entrepris. Un service composé est déclaré correct s’il respecte un ensemble d’exigences de deux types: les exigences transactionnelles et de QoS (la sécurité des exigences métiers). Les exigences de QoS sont définies sous la forme d’un contrat SLA (service-level agreement). Un contrat SLA est un ensemble de contraintes de QoS. Les exigences transactionnelles sont spécifiées par les concepteurs en utilisant le concept d’états de terminaison acceptés (ETA). Un logiciel composite FOSS est dit correct s’il respecte un ensemble de contraintes de dépendances et de capacités. Pour parvenir à résoudre ce problème de vérification, nous proposons une approche formelle fondée sur la méthode Event-B. Une telle approche se résume en deux points: i) Une formalisation Event-B de la composition de services avec Event-B. ii) Une formalisation Event-B de la composition de logiciels FOSS dans un contexte cloud. Ces deux formalisations sont validées en se servant des obligations de preuves et d’un model-checker ProB. La formalisation de la composition de services se repose sur les trois étapes suivantes: - Etape 1: formalisation des services Web. - Etape 2: formalisation de la composition statique de services Web. - Etape 3: formalisation de la composition dynamique de services Web. Quant à la deuxième formalisation, elle est construite en deux étapes principales. La première étape concerne la formalisation des logiciels FOSS composites d’une manière générale. Dans la deuxième étape, on raffine cette formalisation par l’introduction des propriétés d’élasticité verticale et horizontale offertes par l'environnement cloud. La propriété d'élasticité verticale permet d'augmenter ou de réduire la capacité des logiciels en ajoutant de nouvelles ressources (logiciels) ou en supprimant celles qui ne sont pas en cours d’utilisation. La propriété d'élasticité horizontale permet d'augmenter ou de diminuer les ressources logicielles en ajoutant de nouvelles copies de composants existants ou en supprimant les inutiles. Pour la mise en œuvre de cette approche nous utilisons une approche à base d’IDM (transformation texte to modèle, modèle to modèle et modèle to texte).
LOVE 01/04/2021 Typing Differentiable Programming, 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:15 - 11:15
Résumé :
Differentiable programming is a recent research area: its objective is to express differentiation as a modular algorithmic transformation on rich programming languages. It is in particular motivated by the various applications of automatic differentiation in machine learning or formal calculus. In this talk I will present joint work with Pierre-Marie Pédrot, focusing on the typing system used to express differentiation. We will first review a few examples of differentiable languages recently exhibited in the literature. This allows to identity the linear Dialectica transformation as a reverse automated differentiation transformation on a higher-order lambda-calculus with positive types. Building on the intuitions provided by Dialectica and distribution theory, we construct a lambda-calculus with an internal differentiation operator. This calculus is typed by a type system inspired by Differential Linear Logic. Noticeably, we are able to express backward automatic differentiation as an evaluation strategy.
LOVE 30/03/2021 Reducing the Security Assessment for Industrial Cyber-Physical Systems against Smart Attacks , par Samir Ouchani
Samir Ouchani, Lineact CESI (Aix-en-Provence, France)  
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
30/03/2021    10:30 - 11:30
Résumé :
Industrial cyber-physical systems (ICPS) are heterogeneous inter-operating parts that can be physical, technical, networking, and even social-like agent operators. Incrementally, they perform a central role in critical and industrial infrastructures, governmental, and personal daily life. Especially with the Industry 4.0 revolution, they became more dependent on connectivity by supporting novel communication and distance control functionalities, which expand their attack surfaces that result in a high risk for cyber-attacks. Further, regarding physical and social constraints, they may push up new classes of security breaches that might result in serious economic damages. Thus, designing a secure ICPS is a complex task that has to guarantee security and harmonize the functionalities between the various parts that interact with different technologies. This talk highlights the significance of cyber-security infrastructure and shows how to evaluate, prevent, and mitigate ICPS-based cyber-attacks. First, I will take this opportunity to introduce myself and briefly present my ongoing research activities. Then, I will present the foundation of a prominent semantics for ICPS’s entities and their composition, which includes social actors that act differently than mobile robots and automated processes. In addition, I will provide the feasible attacks generated by a reinforcement learning mechanism based on multiple criteria that selects both appropriate actions for each ICPS component within the possible countermeasures for mitigation. Finally, I will detail the overall solution that reduces the verification cost and its effectiveness in a real use case scenario.
LOVE 19/03/2021 Avancées récentes sur les algèbres de Kleene concurrentes, par Paul Brunet
Paul Brunet, University College London  
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
19/03/2021    10:30 - 11:30
Résumé :
Les algèbres de Kleene concurrentes (CKA) fournissent un cadre algébrique pour raisonner sur les programmes concurrents. Au cours de ces dernières années, nous avons étudié différentes manières d'enrichir ce modèle afin de capturer une classe plus large de problèmes de vérification. Dans cet exposé, je présenterai tout d'abord les bases de CKA, avec ses présentations axiomatiques et combinatoires, et les résultats de décidabilité correspondants. Je ferais ensuite un bref panorama de certaines extensions du modèle, en considérant des aspects tels que le flot de contrôle, la cohérence des accès mémoire, et l'exclusion mutuelle. Ce travail est le fruit de collaborations avec Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, et Georg Struth.
LOVE 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.
LOVE 18/03/2021 Model-checking pour l’agriculture de précision, par Rim Saddem
Rim Saddem  
https://bbb.lipn.univ-paris13.fr/b/ari-uht-t3u
18/03/2021    14:00 - 15:00
Résumé :
Dans cette présentation, je vais vous présenter mon travail de recherche qui comporte deux parties : la première porte sur ce que j’ai effectué durant ma thèse et la deuxième porte sur ce que j’ai effectué durant mon poste ATER. Mon travail de thèse porte sur l’application des techniques de model-checking pour résoudre des problèmes issus de l’agriculture de précision. L’agriculture de précision (AP) s’est fortement développée au cours des dernières décennies avec les progrès des technologies de localisation, des capteurs et des techniques de télédétection. Le principe de l’AP est de rechercher et mettre en œuvre la Bonne action au Bon moment et au Bon endroit ("3B"), avec l’objectif d’améliorer l’efficience de l’agriculture suivant les critères d’une agriculture durable. Pour modéliser et vérifier des opérations agricoles, une représentation des dynamiques temporelles et spatiales est nécessaire. Le model- checking de systèmes d’automates temporisés avec des requêtes dans une logique temporelle arborescente répond à ces besoins, les positions spatiales pouvant être représentées de façon ad-hoc dans le cadre de ces formalismes. Trois exemples d’opérations agricoles ont été considérés dans ce travail. La première est relative au calcul d’une séquence optimale de commandes pour une pulvérisation de précision en viticulture. La seconde concerne la récolte sélective en viticulture. La dernière est relative à la vérification d’une mission de robotique agricole. Nous étudions dans ces exemples l’atteignabilité d’un état cible pour l’opération, ou l’atteignabilité avec un critère de coût optimal. Pour pallier au problème d’explosion combinatoire rencontré dans les cas traités, une méthodologie de décomposition pour le model-checking d’atteignabilité a été développée. Les résultats expérimentaux avec et sans décomposition sont présentés pour les 3 exemples d’opération étudiés. La technique de décomposition est appliquée sur 2 des 3 exemples et les résultats expérimentaux montrent son efficacité. Mon travail durant mon poste ATER propose une extension du formalise des processus métiers pour prendre en considération la représentation spatiale afin de modéliser le comportement des robots.
LOVE 18/03/2021 Transcendental Syntax: the dynamics of logic programs and tilings, applied to Linear Logic, 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é :
The Transcendental Syntax, successor of Girard's Geometry of Interaction programme, aims at a reconstruction of linear logic from computation with finite objects. We define a model of computation we call Stellar Resolution; a graph-theoretical reformulation of Robinson's first-order resolution, which appear to be closely related to geometric tilings. As a first illustration of the Transcendental Syntax's technical content, we show that we can naturally encode both the cut-elimination and logical correctness of MLL proof-structures. Using techniques from realisability, similarly to ludics, we retrieve a very generic notion of linear typing as a description of computational behaviour for programs computing with local and asynchronous interactions.
AOC 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.
AOC 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.
LOVE 11/03/2021 [Séminaire Chocola] Machine-Checked Computer-Aided Mathematics, par Assia Mahboubi
Assia Mahboubi, INRIA  
https://chocola.ens-lyon.fr/events/seminaire-2021-03-11/
11/03/2021    10:00 - 12:00
Résumé :
This talk presents an overview of three contributions to the formal verification of mathematics in dependent type theory. The first of these contributions deals with the realization of a library of digitized mathematics, covering the standard undergraduate background in algebra as well as some more advanced chapters in finite group theory. The two other contributions are related to the issues pertaining to the formal verification of computational mathematical proofs, by the means of symbolic algorithms and of rigorous numerical methods respectively. We conclude with a few perspectives on the formal verification of computer-aided mathematics.
LOVE 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.
LOVE 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.
LOVE 04/03/2021 Geometry of Interaction for ZX-Diagrams, par Kostia Chardonnet et Renaud Vilmart
Kostia Chardonnet et Renaud Vilmart, LRI  
https://bbb.lipn.univ-paris13.fr/b/sei-eer-t24 (code d'accès: 749983)
04/03/2021    10:30 - 11:30
Résumé :
ZX-Calculus is a versatile graphical language for quantum computation equipped with an equational theory. Getting inspiration from Geometry of Interaction, in this work we propose a token-machine-based asynchronous model of both pure ZX-Calculus and its extension to mixed processes. We also show how to connect this new semantics to the usual standard interpretation of ZX-diagrams. This model allows us to have a new look at what ZX-diagrams compute, and give a more local, operational view of the semantics of ZX-diagrams.
LOVE 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é :
AOC 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.
LOVE 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.
AOC 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.
LOVE 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.
LOVE 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.
LOVE 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).
AOC 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.
LOVE 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.
LOVE 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.
LOVE 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.
LOVE 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.
LOVE 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.
LOVE 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.
AOC 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
LOVE 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.
RCLN 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..)
AOC 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.
AOC 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.
LOVE 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.
AOC 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.
LOVE 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.
LOVE 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.
AOC 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.
LOVE 05/11/2020 Journée Opérades LIPN-LAGA, par Conférence
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).
LOVE 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.
LOVE 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.
LOVE 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.
RCLN 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.
LOVE 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.
LOVE 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.
RCLN 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.
LOVE 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.
LOVE 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.
LOVE 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.
LOVE 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.