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

Afficher les séminaires de

Séminaires à venir
A3 05/09/2019 Redescription en analyse de données : exemples variés., par François Rioult
François Rioult , Greyc, Université de Caen  
Salle B107, bâtiment B, Université de Villetaneuse
05/09/2019    12:15 - 13:45
Résumé :
Le thème général de cette présentation est la redescription des données dans un espace où elles peuvent être prises en charge par des techniques éprouvées d'apprentissage automatique. Par exemple, pour prédire un événement dans une séquence, on peut la recoder comme succession de motifs fermés. D'autres exemples seront abordés, comme la transformation d'un ensemble de règles en un graphe, de trajectoires de joueurs d'une équipe en trajectoire d'un polygone, ou encore d'un spectre sonore en image pour de la classification en deep learning.
AOC 17/09/2019 Algorithmes auto-stabilisants, par Lélia Blin
Lélia Blin, Sorbonne Université LIP6  
Salle B107, bâtiment B, Université de Villetaneuse
17/09/2019    12:30 - 13:30
Résumé :
Dans le contexte des réseaux à grande échelle, la prise en compte des pannes est une nécessité. L'auto-stabilisation est une approche algorithmique de la tolérance aux pannes dans les systèmes distribués dont le but est de gérer la corruption de la mémoire des processeurs dues à des pannes transitoires. Plusieurs paramètres caractérisent l'efficacité d'un algorithme auto-stabilisant, dont en particulier (1) le temps pris par le système pour retourner dans une configuration légale suite à une corruption arbitraire de la mémoire de ses processeurs, et (2) l'espace mémoire utilisé par les processeurs pour exécuter l'algorithme. La minimisation de l'espace mémoire est motivée pas de nombreux aspects : existence de réseaux (tels que les réseaux de capteurs) offrant des espaces mémoires limités, la minimisation des échanges de données entre processeurs voisins, la limitation du stockage d'information afin de pouvoir utiliser des techniques de redondance, etc. Ce séminaire présentera l'auto-stabilisation au travers deux grands problèmes classiques : la construction d'arbres couvrants, notamment d'arbres couvrants de poids minimum, et l'election d'un leader. Il présentera en particulier les liens entre auto-stabilisation et les techniques de décision distribuée, incluant le calcul de bornes inférieures sur l'espace mémoire nécessaire à la résolution par des algorithmes auto-stabilisants des problèmes susmentionnés.
AOC 24/09/2019 Quelques problèmes d'optimisation dans les réseaux, par Cedric Bentz
Cedric Bentz, CNAM  
Salle B107, bâtiment B, Université de Villetaneuse
24/09/2019    12:30 - 13:30
Résumé :
J'évoquerai dans cet exposé quelques problèmes d'optimisation dans les réseaux auxquels je me suis intéressé, parfois en collaboration avec d'autres chercheurs, depuis quelques années. Dans certaines des variantes étudiées, les réseaux considérés peuvent être sujets aux pannes, ce qui peut nécessiter d'en tenir compte lors de la conception de tels réseaux. La première famille de problèmes étudiés tourne autour de généralisations du problème de multicoupe, prenant notamment en compte le fait que le bon fonctionnement d'un réseau peut être mis en cause même si seul un certain nombre des communications à assurer sont affectées, pour lesquelles des résultats de complexité paramétrée ont été récemment obtenus dans différents cas particuliers. La seconde famille tourne autour de problèmes de d-bloqueurs dans les graphes, dans lesquels on s'intéresse au nombre minimum de noeuds (sommets) ou de liens (arêtes) qui doivent tomber en panne pour que, intuitivement, le réseau descende en-dessous d'un certain seuil de fonctionnement. Plusieurs résultats de complexité notables ont ainsi été obtenus pour cette catégorie de problèmes, dont on ne sait souvent même pas déterminer facilement s'ils sont dans NP ou non. Enfin, la troisième et dernière famille tourne autour de problèmes d'arbres et de réseaux de Steiner, en présence de capacités, et dans certains cas de pannes. Concernant le problème d'arbre de Steiner avec capacités sur les arcs mais sans pannes, les résultats de complexité qui ont été obtenus permettent d'obtenir une caractérisation complète de la complexité de ce problème vis-à-vis de plusieurs paramètres. Concernant le problème de conception de réseaux de Steiner avec capacités et pannes, plusieurs formulations le modélisant, dont une formulation biniveau, ont été obtenues et comparées entre elles, de façon théorique comme expérimentale, et quelques inégalités permettant de les renforcer ont également été testées. Ces formulations peuvent toutes être adaptées au cas où l'on ajoute la possibilité de protéger un certain nombre de liens du réseau, mais un fait notable et pas nécessairement intuitif est que les relations entre les formulations diffèrent alors du cas précédent.
Séminaires passés
MERCRED 03/07/2019 The Robust Capacitated Facility Location Problem, par Marco Caserta
Marco Caserta, IU Business School  
Salle B107, bâtiment B, Université de Villetaneuse
03/07/2019    14:00 - 15:00
Résumé :
We present robust formulations for the capacitated facility location problems under demand uncertainty, both for the single-source and the multi-source variants. Robustness is defined over different uncertainty sets, i.e., the box, ellipsoidal, and polyhedral uncertainty sets. For each of these variants, we define the robust counterpart and we compare the results obtained through an extensive computational study. We test the effect of using different support sets and analyze the performance of each robust variant using scenario curves and price of robustness, among other measures.
AOC 02/07/2019 Aspects combinatoires du problème de l'UCP, par Pierre Fouilhoux
Pierre Fouilhoux, Lip6 - Paris 6 - Sorbonne Université  
Salle B107, bâtiment B, Université de Villetaneuse
02/07/2019    12:30 - 13:30
Résumé :
Le problème classique appelé Unit Commitment Problem (UCP) est le problème central de planification de production d'électricité. Le problème combinatoire au coeur du problème de l'UCP est appéle le Min-up/min-down UCP (MUCP). Il consiste à déterminer un plan de production sur un horizon de temps discrétisé, pour un ensemble de centrales électriques. A chaque pas de temps, la production totale doit répondre à une demande connue. Chaque unité doit satisfaire des contraintes de temps minimum de fonctionnement et d'arrêt. Elle correspond également à des coûts de production et de mise en marche. Nous étudions comment la complexité du MUCP évolue en fonction du nombre d'unités et de période. Nous montrons en particulier que ce probl&egrav e;me est NP-difficile au sens fort. Nous présentons plusieurs aspects polyédraux d'une formulation PLNE pour le MUCP en nous intéressant à la combinatoire liant la production des unités entre les pas de temps. Pour cette formulation, l'espace des solutions exploré par un algorithme de branchement contient de nombreuses solutions symétriques et sous-symétriques: deux solutions symétriques (resp. sous-symétriques) pouvant être obtenues l'une de l'autre par permutation de ses composantes (resp. d'une partie de ses composantes). Nous proposons deux techniques bien distinctes pour briser ces symétries et accélérer la résolution. La première technique s'appuie sur l'étude du polyèdre des permutations et sur un algorithme, dit de fixing, utilisé à chaque noeud de l'algorithme de branchement. La deuxième technique repose sur des inégalités linéaires et des variables additionnelles. Enfin, nous présentons plusieurs aspects prometteurs sur une nouvelle décomposition de Dantzig-Wolfe qui utilise plusieurs inégalités issues de notre étude polyèdrale. Travaux réalisés avec Pascale Bendotti et Cécile Rottner.
MERCRED 26/06/2019 La Maison des Maths d'Ispahan, par Amir Hashemi
Amir Hashemi, Université Technologique d'Ispahan  
Salle B107, bâtiment B, Université de Villetaneuse
26/06/2019    14:00 - 15:00
Résumé :
Dans une première partie, je présenterai le système de recherche et enseignement supérieur des universités iraniennes et discuterai de ses performances. Dans une seconde partie, je présenterai les missions et activités des Maison des Mathématiques iraniennes, dont la première a été établie en 1999 à Ispahan. Il s'agit donc d'un exposé non technique, plutôt meta-scientifique. Il sera accompagné de quelques gâteaux iraniens.
AOC 25/06/2019 Optimisation et Bicliques, par Denis Cornaz
Denis Cornaz, LAMSADE - Paris Dauphine  
Salle B107, bâtiment B, Université de Villetaneuse
25/06/2019    12:30 - 13:30
Résumé :
Un sous-graphe partiel, d'un graphe donné, est une biclique, de ce graphe, s'il est biparti complet. D'abord, nous passerons en revue des résultats classiques admettant des preuves élégantes, voir surprenantes, autour de cette notion. Ensuite, nous mènerons une étude structurelle, particulière à cette notion, permettant de mettre en œuvre une technique générale d'optimisation (branch-and-cut, -and-price). Nous terminerons par une conjecture récemment démontrée.
RCLN 24/06/2019 Identity links in knowledge graphs, par Nathalie Pernelle
Nathalie Pernelle, LRI, Université Paris Sud  
Salle B107, bâtiment B, Université de Villetaneuse
24/06/2019    16:00 - 17:00
Résumé :
As the Web of Data continues to grow, more and more large datasets – covering a wide range of topics and domains – are being added to the Linked Open Data (LOD) Cloud. It is inevitable that different datasets, most of which are developed independently of one another, will come to describe (aspects of) the same thing, but will do so by referring to that thing by different names. Thanks to identity links, datasets that have been constructed independently of one another are still able to make use of each other’s information. Many data linking approaches have been defined that are rule-based. Some of these approaches exploit ontology axioms such as keys. However, these axioms are rarely specified in the available ontologies. In this seminar, I will present two approaches that aim to discover more or less expressive keys in RDF data. Then, since data linking approaches do not obtain a 100% precision, I will show that some approaches can focus on detecting incorrect sameAs links or detect that they are valid only in a specified semantic context.
A3 19/06/2019 Data Explainability Through Linguistic Expression of Extracted Knowledge, par Marie-Jeanne Lesot
Marie-Jeanne Lesot, LIP6  
Salle B107, bâtiment B, Université de Villetaneuse
19/06/2019    12:15 - 13:30
Résumé :
The pervasive use of data science techniques extracts regularities from available data for different tasks, such as prediction, characterisation or structuring. A current challenge is to improve the legibility of the obtained results, so as to allow a data expert to understand better the content of the data. One way to address this challenge consists in presenting them in natural language, offering linguistic expressions which may be easier to interpret for the user. The choice of such a result formulation then has an impact on the machine learning techniques to be applied to the data. The talk will illustrate these questions for numerical data as well as for time series, respectively discussing the extraction of gradual itemsets, that linguistically express knowledge about feature covariations, and the extraction of periodicity-related linguistic summaries, using the specific quantifier “regularly”. In both cases, as well as for enriched contextual variants, the question is to define precisely the associated semantics and to design efficient extraction algorithms. The talk will also discuss the issue of measuring the relevance of the linguistic terms used to express the summaries, both with respect to the data structure, in case of linguistic variables, and with respect to the cognitive interpretation, in case of approximate numerical expressions.
LOVE 18/06/2019 Parametric schedulability analysis of a launcher flight control system under reactivity constraints, par Jawher Jerray
Jawher Jerray, Équipe LoVe, LIPN  
Salle A303
18/06/2019    13:00 - 13:30
Résumé :
The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. We present an approach on the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We describe the problematic of the scheduling of a launcher flight control, then we show how this problematic can be formalized with parametric stopwatch automata; we then present the results computed by IMITATOR.
LOVE 18/06/2019 Towards parallel verification of concurrent systems using the Symbolic Observation Graph, par Hiba OUNI
Hiba OUNI, Équipe LoVe, LIPN  
A303
18/06/2019    12:30 - 13:00
Résumé :
An efficient way to cope with the combinatorial explosion problem induced by the model checking process is to compute the Symbolic Observation Graph (SOG). Given a stutter-invariant event-based LT L formula ?, involving a subset of actions (called observable actions), the SOG is a condensed representation of the state space graph based on a symbolic encoding of the nodes (sets of states linked with unobservable actions) and an explicit representation of the edges (labelled with observable actions). It has the advantage to be much reduced comparing to the original state space graph while being equivalent with respect to stutter-invariant temporal properties (i.e., the original system satisfies ? if and only if the corresponding SOG satisfies ?). Aiming to go fu rther in the process of tackling the state space explosion problem, we propose in this paper to parallelize the construction of the SOG using a hybrid approach (distributed+shared memory). Doing so, we take advantage of the recent advances in computer hardware, by distributing the construction process over a large number of multi-core processors. We studied the performances of our new approach comparing to both distributed and shared memory approaches on one side, and to the sequential construction on the other side. The obtained results show that the proposed approach offers an interesting alternative allowing to completely exploit the available distributed architecture while offering significant speedup.
LOVE 13/06/2019 La logique du signe : Sémiologie structuraliste et typage par biorthogonalité pour l'analyse de corpus., par Juan Luis Gastaldi
Juan Luis Gastaldi, ETH Zürich, SPHERE Paris Diderot  
Salle B107, bâtiment B, Université de Villetaneuse
13/06/2019    10:30 - 12:30
Résumé :
Dans cette conférence, il s'agira de présenter le cadre théorique et conceptuel d'une recherche en cours associant le projet d'une théorie formelle du signe d'inspiration structuraliste à certains principes et ressources de la linguistique de corpus et de la logique linéaire. L'objectif de ce travail interdisciplinaire est d'inférer de façon non supervisée des structures grammaticales ou logiques émergentes pour tout système de signes donné sous la forme d'un corpus d'expressions. L'analyse formelle proposée se base sur une procédure de segmentation stratifiée et de typage par biorthogonalité, capable, en principe, de capturer des structures de tous les niveaux (phonologiques ou graphématiques, morphologiques, syntaxiques et sémantiques). D'un point de vue philosophique, la perspective adoptée implique une manière originale de rapporter la logique au langage et à d'autres systèmes naturels de signes.
MERCRED 05/06/2019 Alice au pays des frises et des pavages, par François Bergeron
François Bergeron, UQAM  
Salle B107, bâtiment B, Université de Villetaneuse
05/06/2019    14:00 - 15:00
Résumé :
La notion de frise d’entiers a été introduite dans les années 1970 par Conway et Coxeter. Une telle frise correspond à un nombre fini de bandes horizontales superposées d’entiers positifs (>0), bornées au-dessus et en dessous par des bandes de 1, avec une condition locale liant ces entiers. Plus explicitement on demande que ad-bc=1, pour toute configuration locale de a, b, c, et d en forme de «?diamant?» (a et d se suivent sur une même ligne, avec b et c respectivement juste au-dessus et en dessous). Conway et Coxeter ont souligné que cela force un phénomène de répétition cyclique horizontale; de là le terme de frise. Un autre aspect fascinant est qu’ il n’y a qu’un nombre fini de telles frises ayant un nombre fixé de lignes, et qu’elles sont énumérées par les nombres de Catalan. Après un survol de cette notion et de sujets reliés, nous allons en considérer diverses généralisations. En particulier, on établira des liens avec la formule de condensation de Dogdson (l’auteur d’Alice au pays des merveilles) pour un calcul récursif de déterminants.
LOVE 23/05/2019 Towards a Combinatorial Proof Theory, par Ben Ralph
Ben Ralph, Inria Saclay  
Salle B107, bâtiment B, Université de Villetaneuse
23/05/2019    14:00 - 16:00
Résumé :
Combinatorial proofs have been introduced by Hughes to give a ``syntax-free'' presentations for proofs in classical propositional logic. In a nutshell, a classical combinatorial proof consists of two parts: (i) a linear part, and (ii) a skew fibration. The linear part encodes a proof in multiplicative linear logic (MLL), whose conclusion is given represented in a cograph, while the skew fibration maps this linear cograph to the cograph of the conclusion of the whole proof. For deep inference proofs, this skew fibration corresponds exactly to a contraction-weakening derivation. Applying certain restrictions to these two rules leads to substructural logics and substructural proof theory. These proof theoretic restrictions correspond precisely to set-theoretic and graph-theoretic restrictions on the skew fibration, allowing us to characterise proof systems by their graph homomorphism class.
A3 23/05/2019 Universal and best approximation through Bayesian ARTMAP, par Lucian SASU
Lucian SASU, Transilvania University of Brasov (Romenia)  
Amphi Ampere
23/05/2019    14:00 - 15:30
Résumé :
Bayesian ARTMAP is an adaptive resonance-theory based model, which was extended to perform regression. The network is shown to have both universal and best approximation properties. The network architecture and learning algorithm are presented, along with sketches of proofs and open questions.
LOVE 23/05/2019 Rigid species and normal functors over groupoids , par Zeinab Galal
Zeinab Galal, IRIF  
Salle B107, bâtiment B, Université de Villetaneuse
23/05/2019    10:30 - 12:00
Résumé :
Species of structures were introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics. Species are connected to Girard's normal functor semantics of ?-calculus where terms are interpreted as power series with sets as coefficients. Fiore et al. presented a generalised definition that both encompasses Joyal's species and constitutes a model of differential linear logic (DiLL). For generalised species of structures, types are interpreted as groupoids which provides the connection with combinatorics whereas they are interpeted as sets in Girard's normal functors. To investigate how these models interact, we show that all the interpretations of proofs in DiLL actually live in a smaller fragment of generalised species called rigid species. These species correspond to the concept of free groupoid actions which provides us with a notion of normal functors over groupoids and allows us to bridge the gap between species and normal functors.
MERCRED 22/05/2019 Theoretical and Applied Research in Machine Learning, par Lucian SASU
Lucian SASU, Transilvania University of Brasov, Roumanie  
Salle B107, bâtiment B, Université de Villetaneuse
22/05/2019    14:00 - 14:45
Résumé :
Some insights and experiences in theoretical and applied research are shared. The two worlds are quite different and complementary. The presentation exposes challenging topics in industry which can be addressed through ML, along with hints for researchers willing to join industrial R&D departments.
RCLN 17/04/2019 Résumé de texte translingue par compression, par José Manuel Torres-Moreno
José Manuel Torres-Moreno, LIA, U.Avignon  
Salle B107, bâtiment B, Université de Villetaneuse
17/04/2019    14:30 - 15:30
Résumé :
Le Résumé Translingue de Textes (RTT) vise à générer un résumé dans une langue autre que le document source. Plus précisément, le RTT consiste à analyser un document dans une langue source pour en extraire sa signification, puis à générer un résumé court, informatif et correct dans une langue cible. Ce processus peut être divisé en deux processus principaux : le résumé et la traduction. Processus souvent antagonistes. Nous avons développé un cadré expérimentale pour générer des résumés translingues de documents en anglais, français, portugais, espagnol vers {anglais, français}. Nous avons utilisé des applications du TALN (résumé par extraction, similarité de phrases, compression de phrases et fusion multi-phrases) et des approches neuronales pour construire nos modèles de RTT. Cette présentation sera ciblée sur les techniques et les résultats obtenus lors de nos expériences.
LOVE 16/04/2019 Run-time Monitoring Approach for Hardware Trojans Dectection, par Maha Naceur
Maha Naceur, Université Paris 13  
Salle A303, bâtiment A, Université de Villetaneuse
16/04/2019    12:30 - 13:30
Résumé :
Today’s integrated circuits are vulnerable to malicious activities and alterations such as Hardware Trojan Horses (HTH), which can alter the functioning of the circuit, either during design or fabrication. Run-time monitoring is a predominantly used technique to validate a design in industry. Formal veri?cation overcomes the weakness of exhaustive simulation by applying mathematical methodologies to prove design correctness in an automated way. The design is analysed only against their functional characteristics, and their parametric behavior are do not considered in order to analyze the effects of HTHs. In this work, we present a new approach which focuses upon a combined technique that integrates the best characteristics of both run-time monitoring and formal veri?cation methods to provide an effective design validation tool which uses assertions to automatically generate synthesizable monitors capable for detecting hardware trojan horses at runtime
RCLN 04/04/2019 Apprentissage automatique à partir de données complexes et dynamiques: Application aux données textuelles, par Parisa RASTIN
Parisa RASTIN, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
04/04/2019    13:30 - 14:30
Résumé :
Les données actuelles sont de plus en plus variées et complexes et il est en général nécessaire d’adapter les algorithmes d’analyse à chaque type de description des données. Les algorithmes d’apprentissage devraient cependant pouvoir être fonctionnels quel que soit le type des données et la métrique choisie. Nous présentons dans cet exposé un algorithme de clustering relationnel basée sur le système de Coordonnées Barycentriques pour homogénéiser la représentation des objets et des prototypes et traiter de grands ensembles de données complexes. Dans le système de Coordonnées Barycentriques, l’espace de représentation est défini par un ensemble unique de points de support choisis parmi les objets de la base d'apprentissage. La définition d’un prototype correspond au calcul d’un objet dans l’espace barycentrique. À partir de ces approches, nous proposons un algorithme d'apprentissage basé sur un réseau de neurones artificiel défini dans l'espace barycentrique, adapté aux flux de données textuelles et permettant un suivit dynamique de l'évolution des données au cours du temps. Nous présenterons une applications concrètes sur l’extraction de domaines d’intérêt extraits d’URLS à partir de trace de navigation en ligne.
LOVE 02/04/2019 Continuous models of computation: computability, complexity,, par Amaury Pouly
Amaury Pouly, IRIF  
Amphy Ampère
02/04/2019    14:00 - 15:30
Résumé :
Et un cours abstract si nécessaire: In 1941, Claude Shannon introduced a continuous-time analog model of computation, namely the General Purpose Analog Computer (GPAC), [which can be implemented in practice through the use of analog electronics or mechanical devices]. In this talk, we review some recents results on the link between the GPAC and Turing machines. We will also see a surprising result on universal polynomial differential equations. Finally, I will also mention some recent application of this work to show that chemical reaction networks are strongly Turing complete with the differential semantics.
LOVE 02/04/2019 Fault-tolerant matrix factorisation: a formal model and proof, par Daniel Torres
Daniel Torres, LIPN, Équipe LoVe  
Salle A303, bâtiment A, Université de Villetaneuse
02/04/2019    12:30 - 13:30
Résumé :
As the size of high performance systems grows, tolerating failures has become a major issue in parallel computing. In this paper, we present a Coloured Petri Net model for a fault tolerant matrix factorisation algorithm. On the model, we prove resiliency properties and completion of the algorithm in presence of failures whatever the size of the input. This illustrates how formal modelling and verification techniques can help designing proofs on distributed algorithms.
27/03/2019 Journée IA du LIPN
 
Amphi Euler
27/03/2019    09:00 - 18:00
Résumé :
Cette journée est organisée par le Laboratoire d’Informatique de Paris Nord LIPN a pour but de présenter des travaux en intelligence artificielle, soit réalisés par des chercheurs du LIPN soit réalisés par des chercheurs extérieurs aussi bien académiques qu’industriels. Cette journée aura lieu dans l’amphithéâtre Euler de l’institut Galilée. L’inscription est gratuite mais obligatoire.
LOVE 19/03/2019 The size-change principle for mixed induction and coinduction, par Pierre Hyvernat
Pierre Hyvernat, Lama (Université de Savoie, Chambéry)  
C 304
19/03/2019    14:00 - 16:00
Résumé :
The Size-Change Principle (SCP) is a simple algorithm giving a partial termination test for recursive definitions. If the language is lazy, it also gives (by duality) a partial productivity test for recursive functions involving coinductive types. This is what is used in Agda. Unfortunately, when inductive and coinductive types are nested, this is unsound: there are "well typed" and terminating recursive definitions producing terms in empty types. Such definitions make Agda inconsistant. Using ideas from L. Santocanale about circular proof and parity games, I'll show how the SCP can be used to check "totality" of recursive definitions. Besides the SCP, the main ingredient is a more informative of call-graph, and I'll sketch the proof of correctness by defining their semantics using power domains.
LOVE 19/03/2019 Modeling, Analysis and Design of Critical Systems, par Prof. Nejib Ben Hadj-Alouane
Prof. Nejib Ben Hadj-Alouane, National Engineering School of Tunis (ENIT) - OASIS Lab (Optimization, Analysis of Industrial Systems and Services)  
Salle A303, bâtiment A, Université de Villetaneuse
19/03/2019    12:30 - 13:30
Document attaché
Résumé :
Our work on critical systems targets a number of problem areas and applications, all requiring the development of models for analysis and verification, and tools for decision making. This talk focuses on four different problem areas, each requiring a different modeling framework and solution approach. We begin by exposing our new Petri nets modeling framework, Extended Timed Petri Nets (ETPN), useful in modeling a special class of hybrid systems, with a weak continuous component and a strong discrete one, encountered when dealing with modern man-made, embedded and real-time systems. We discuss a supervisory control problem based on this framework, along with other related issues dealing with model transformation and complexity. Our second problem addresses operating high-demand and high-performance virtualized data centers (DCs). We focus on the development of tools, based on operations research models and techniques, for the management of theses DCs, while striving to improve user applications performance and productivity. We focus on the problem of virtual machines (VMs) placement in geographically distributed data centers. We consider communicating VMs assigned to data centers that are connected via a backbone network. We aim to plan and optimize the placement of VMs in data centers so as to minimize the IP-traffic within the backbone network along with user service interruption. Our third problem deals with security and in computer systems, services and protocols. We use the property of opacity to capture secrecy-related problems. We focus on the development of an on-line method for the efficient verification of opacity in models based on automata. We also extend opacity with the introduction of a quantification measure. Our fourth problem deals with sensor networks and their use in precision agriculture. We show that the development of application-oriented infrastructure management techniques, such a routing protocols, is important for modern Fog/IoT networks. Throughout our talk we discuss several research perspectives and applications linked to modern technologies, such as IoT, Web Services and Cloud/Fog computing.
LOVE 19/03/2019 Inequalities between plethysm coefficients and Kronecker coefficients via geometric complexity theory, par Christian Ikenmeyer
Christian Ikenmeyer  
Salle B107, bâtiment B, Université de Villetaneuse
19/03/2019    10:30 - 12:00
Résumé :
Research on Kronecker coefficients and plethysms gained significant momentum when the topics were connected to geometric complexity theory, an approach towards computational complexity lower bounds via algebraic geometry and representation theory. Both types of coefficients appear independently in R. Stanley's list of "Positivity problems and conjectures in algebraic combinatorics". This talk is about a result that was obtained with geometric complexity theory as motivation, namely an inequality between rectangular Kronecker coefficients and plethysm coefficients. The proof interestingly uses insights from algebraic complexity theory. As far as we are aware, algebraic complexity theory has never been used before to prove an inequality between representation theoretic multiplicities. This is joint work with Greta Panova (Rectangular Kronecker coefficients and plethysms in geometric complexity theory, Adv Math 2017).
RCLN 11/03/2019 Structure Prediction Energy Network (SPEN) using Dual Decomposition on Dependency Parsing, par Xudong ZHANG
Xudong ZHANG, LIPN - RCLN  
Salle B107, bâtiment B, Université de Villetaneuse
11/03/2019    14:00 - 15:00
Résumé :
Dependency Parsing is one of the basic tasks in the field of Natural Language Processing (NLP). The goal is to find whether there exist a strong relationship between different words in a sentence. It can be used as the basic step of many NLP systems like question answering system. Solving a dependency parsing problem can be realized by a energy based network with the output of the neural network as a scalar (energy). The goal is to find the most compatible structure (a graph) with the input sentence and the most compatible structure is supposed to give the lowest energy for the neural network. As the structure of the sentence should be a tree (one root, every word has and only has one pa rent, no circle), to simplify the problem, people always construct a linear function corresponding to the structure that we want to find, i.e. we suppose different arcs are independent. However, this method may limit the capacity of the system to describe more complex relations. In this project, inspired by the idea of Structure Prediction Energy Network (SPEN), we construct a new neural network which is composed of two parts, i.e. local energy part and global energy part. We showed that it is possible to solve the problem with dual decomposition when we have a convex (non-linear) function for the global energy part together with the linear local energy part. As one part of my Phd thesis, this work is still ongoing.
A3 28/02/2019 Apprentissage statistique dans un contexte décentralisé et applications à la vision par ordinateur, par David Picard
David Picard, ENSEA Cergy-Pontoise  
Salle B107, bâtiment B, Université de Villetaneuse
28/02/2019    12:15 - 13:45
Résumé :
L'apprentissage statistique est de nos jours incontournable dans un certain nombre de tâches complexes, notamment dans le traitement des données multimédia comme la vision. Pour gagner en précision, des modèles de plus en plus complexes sont entraînés sur des volumes de données de plus en plus gros. Cependant, la répartition naturelle des données auprès des capteurs qui les ont crées laisse à penser qu'il serait préférable d'apprendre ces modèles sans collecter les données d'apprentissage auprès d'un calculateur central. Nous présentons dans cet exposé un paradigme d'apprentissage décentralisé asynchrone pour répondre à ce problème. Nous considérons le cas ou plusieurs calculateurs optimisent un modèle statistique à l'aide de données locales et coopèrent afin d'obtenir un modèle consensus. Nous montrons comment transposer des algorithmes d'apprentissage connus (k-means, PCA, SVM, deep learning) à ce paradigme, ainsi que des preuves de leur équivalence avec les versions centralisées. Enfin, nous montrons plusieurs exemples d'applications de ces modèles à des tâches de vision par ordinateur.
LOVE 27/02/2019 Monoides et algèbres de tris sur les groupes de coxeter, par Nicolas Thiéry
Nicolas Thiéry  
B311
27/02/2019    15:22 -
Résumé :

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

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

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

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

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

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

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

(ANNULE pour cause de GREVE)

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

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

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

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

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

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

(ANNULE pour cause de GREVE)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(See also http://www.doc.ic.ac.uk/research/technicalreports/2010/)

This is joint work with James Brotherston (Imperial)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

LOVE 27/02/2019 Quantum programming languages and logical approaches to quantum information theory, par Peter Selinger
Peter Selinger  
B311
27/02/2019    15:22 -
Résumé :

Dans la période du 7 au 17 février 2011, Peter Selinger (Dalhousie University, chercheur invité au LIPN) propose un cycle de séminaires sur

Quantum programming languages and logical approaches to quantum information theory

Le cycle est composé de quatre séances, ouvertes à tous, qui se tiendront au LIPN en salle B311, avec le calendrier suivant :
  • 7 février 2011, 13h30-15h
  • 10 février 2011, 10h-12h
  • 14 février 2011, 13h30-15h
  • 17 février 2011, 10h-12h
LOVE 27/02/2019 Von neumann algebras in physics by examples, par Pierre Martinetti
Pierre Martinetti  
B311
27/02/2019    15:22 -
Résumé :

Le 28 février 2011, à 15h30 en salle B311, le séminaire LCR accueille Pierre Martinetti (Università di Roma - Tor Vergata).

We will illustrate the importance of von Neumann algebras in physics, emphasizing in particular their role in the algebraic formulation of quantum field theory. We will illustrate by various examples how some characteristic properties of von Neumann algebra have a direct translation into properties of spacetime.

LOVE 27/02/2019 From cps to polarisation: a proof-Theoretic decomposition of delimited cps translations, par Guillaume Munch-Maccagnoni
Guillaume Munch-Maccagnoni  
B311
27/02/2019    15:22 -
Résumé :

Le 14 mars 2011, à 15h30 en salle B311, le séminaire LCR accueille Guillaume Munch-Maccagnoni (PPS, Paris 7).

The understanding of continuation-passing style (CPS) translations, an historical source of denotational semantics for programming languages, benefits from notions brought by linear logic, such as focalisation, polarities and the involutive negation. Here we aim to show how linear logic helps as well when continuations are delimited, i.e. return and can be composed, in the sense of Danvy and Filinski.

First we provide a polarised calculus with delimited control (first-class delimited continuations) which is, at the level of computation, a variant of Girard's polarised classical logic LC. It contains variants of delimited control calculi which spawned as answers to the question what order of evaluation can we consider with delimited control. Thus our polarised calculus is one answer which is unifying to some degree.

Subsequently we decompose the calculus through polarised linear logic. The only difference with non-delimited continuations is the use of specific exponentials, that account for the specific semantics of the target of delimited CPS translation, as well as annotations of type-and-effect systems.

As a by-product, we obtain an explanation of CPS translations through a factoring, each step of which accounts for distinct phenomena of CPS translations. Although the factoring also holds for non-delimited CPS translations, it did not appear in its entirety before.

LOVE 27/02/2019 Equivalence entre les analyses mwp et quasi-Interprétations, par Jean-Yves Moyen
Jean-Yves Moyen  
B311
27/02/2019    15:22 -
Résumé :

Le 21 mars 2011, à 15h30 en salle B311, le séminaire LCR accueille Jean-Yves Moyen (LIPN, Paris 13).

Les QI et l'analyse mwp sont deux techniques de complexité implicite pour caractériser Ptime. Les QI travaillent avec des programmes fonctionnels tandis que l'analyse mwp étudie des programmes impératifs.

Je montre, via une transformation de programmes, que bien qu'étant apparemment très différentes ces deux techniques sont moralement équivalentes et capables d'analyser les mêmes cas.

LOVE 27/02/2019 The geometry of multiplicatives and additives: interaction and orthogonality, par Etenne Duchesne
Etenne Duchesne  
B311
27/02/2019    15:22 -
Résumé :

Le 18 avril 2011, à 15h30 en salle B311, le séminaire LCR accueille Etienne Duchesne (LIF, Aix-Marseille 1).

We present a denotational semantics of multiplicative linear logic based on the geometry of interaction. In that semantics, we can define polymorphism using a construction similar to the one of history-free game semantics. We can also present the standard longtrip criterion of proof-nets as an orthogonality relation in the sense of Hyland and Schalk [HS03], and build a category of orthogonality which provides a fully complete model of MLL (without mix).

Besides we extend these constructions polymorphism and orthogonality, to the interpretation of additive connectives.

LOVE 27/02/2019 Estimation of the length of interactions in arena game semantics, par Pierre Clairambault
Pierre Clairambault  
B311
27/02/2019    15:22 -
Résumé :

Le 28 mars 2011, à 15h30 en salle B311, le séminaire LCR accueille Pierre Clairambault (Université de Bath, Royaume Uni).

We estimate the maximal length of interactions between strategies in HO/N game semantics, in the spirit of the work by Schwichtenberg and Beckmann for the length of reduction in simply typed lambda calculus. Because of the operational content of game semantics, the bounds presented here also apply to head linear reduction on lambda terms and to the execution of programs by abstract machines, including in presence of computational effects such as non-determinism or ground type references. The proof proceeds by extracting from the games model a combinatorial rewriting rule on trees of natural numbers, which can then be analysed independently of game semantics or lambda calculus

LOVE 27/02/2019 Theory of von neumann algebras and applications to physics, par Axel de Goursac
Axel de Goursac  
B311
27/02/2019    15:22 -
Résumé :

Le 11 avril 2011, à 15h30 en salle B311, le séminaire LCR accueille Axel de Goursac (Louvain).

We will review the basic theory of von Neumann algebras and see some applications to physics: algebraic quantum field theory, the CKM matrix.

LOVE 27/02/2019 Modèles de taylor pour la résolution du dilemme du fabricant de tables, par Erik Martin-Dorel
Erik Martin-Dorel  
B311
27/02/2019    15:22 -
Résumé :

Le 27 juin 2011, à 15h30 en salle B311, le séminaire LCR accueille Erik Martin-Dorel (LIP, ENS Lyon).

Le Dilemme du fabricant de tables est un problème d'Arithmétique des ordinateurs qui survient lorsqu'on veut implanter une fonction élémentaire (exp, log, sin, cos, arctan, etc.) avec arrondi correct. Exiger que les fonctions mathématiques soient correctement arrondies contribue à accroître la portabilité et la réutilisabilité des logiciels numériques, mais aussi permet de concevoir des algorithmes et des preuves de logiciels qui utilisent cette spécification.

Pour chaque fonction f considérée, la résolution de ce problème dépend de la connaissance des pires cas de f, qui sont les flottants dont l'image par f est très proche du milieu de deux flottants consécutifs. Deux algorithmes (Lefèvre et Stehlé-Lefèvre-Zimmermann) ont été conçus pour énumérer ces pires cas, mais leur temps de calcul avoisinant
plusieurs années-CPU, nous avons d'autant plus envie d'accroître la confiance que l'on peut avoir en leurs résultats.  C'est ce travail de certification qui constitue l'un des principaux buts du projet ANR TaMaDi (Table Maker's Dilemma) [1].

En particulier nous nous intéressons à la validation formelle de l'étape d'approximation polynomiale qui est commune aux deux algorithmes.  Pour ce faire, nous avons entrepris un travail de formalisation avec l'assistant de preuves Coq de ce qu'on appelle les Modèles de Taylor (un polynôme d'approximation + un reste certifié). Notre objectif est de pouvoir calculer des approximants certifiés avec une grande précision, à l'intérieur même de l'assistant de preuves. De plus, nous avons adopté une approche générique fondée sur des calculs par récurrence, vu que la plupart des fonctions élémentaires sont ce qu'on appelle des fonctions holonomes : elles satisfont une équation différentielle linéaire à coefficients polynomiaux, et par
conséquent leurs coefficients de Taylor vérifient une relation de récurrence.

Dans cet exposé, nous présenterons ainsi nos premiers développements réalisés en Coq [2], muni de l'extension SSReflect [3] et de la bibliothèque Coq-Interval [4], elle-même fondée sur la bibliothèque Flocq [5].

Ceci est un travail commun avec Nicolas Brisebarre, Mioara Joldes, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau et Laurent Théry.

Liens :
[1] https://tamadiwiki.ens-lyon.fr/
[2] http://coq.inria.fr/
[3] http://ssr.msr-inria.inria.fr/
[4] http://www.lri.fr/~melquion/soft/coq-interval/
[5] http://flocq.gforge.inria.fr/

LOVE 27/02/2019 Programmation dans les diagrammes de cordes et logique tensorielle, par Paul-André Melliès
Paul-André Melliès  
Amphi Euler
27/02/2019    15:22 -
Résumé :

Dans la période du 4 au 13 juillet 2011, Paul-André Melliès (PPS, CNRS-Paris 7) propose un cycle de séminaires sur

Programmation dans les diagrammes de cordes et logique tensorielle

Le cycle est composé de quatre séances, ouvertes à tous, qui se tiendront à l'Institut Galilée et au LIPN, avec le calendrier suivant :
  • 4 juillet 2011, 14h-16h, amphi Euler (Institut Galilée)
  • 7 juillet 2011, 10h-12h, salle B311 (LIPN)
  • 11 juillet 2011, 14h-16h, salle B311 (LIPN)
  • 13 juillet 2011, 14h-16h, salle B311 (LIPN)
LOVE 27/02/2019 Programmation dans les diagrammes de cordes et logique tensorielle, par Paul-André Melliès
Paul-André Melliès  
B311
27/02/2019    15:22 -
Résumé :

Dans la période du 4 au 13 juillet 2011, Paul-André Melliès (PPS, CNRS-Paris 7) propose un cycle de séminaires sur

Programmation dans les diagrammes de cordes et logique tensorielle

Le cycle est composé de quatre séances, ouvertes à tous, qui se tiendront à l'Institut Galilée et au LIPN, avec le calendrier suivant :
  • 4 juillet 2011, 14h-16h, amphi Euler (Institut Galilée)
  • 7 juillet 2011, 10h-12h, salle B311 (LIPN)
  • 11 juillet 2011, 14h-16h, salle B311 (LIPN)
  • 13 juillet 2011, 14h-16h, salle B311 (LIPN)
LOVE 27/02/2019 Programmation dans les diagrammes de cordes et logique tensorielle, par Paul-André Melliès
Paul-André Melliès  
B311
27/02/2019    15:22 -
Résumé :

Dans la période du 4 au 13 juillet 2011, Paul-André Melliès (PPS, CNRS-Paris 7) propose un cycle de séminaires sur

Programmation dans les diagrammes de cordes et logique tensorielle

Le cycle est composé de quatre séances, ouvertes à tous, qui se tiendront à l'Institut Galilée et au LIPN, avec le calendrier suivant :
  • 4 juillet 2011, 14h-16h, amphi Euler (Institut Galilée)
  • 7 juillet 2011, 10h-12h, salle B311 (LIPN)
  • 11 juillet 2011, 14h-16h, salle B311 (LIPN)
  • 13 juillet 2011, 14h-16h, salle B311 (LIPN)
LOVE 27/02/2019 Programmation dans les diagrammes de cordes et logique tensorielle, par Paul-André Melliès
Paul-André Melliès  
B311
27/02/2019    15:22 -
Résumé :

Dans la période du 4 au 13 juillet 2011, Paul-André Melliès (PPS, CNRS-Paris 7) propose un cycle de séminaires sur

Programmation dans les diagrammes de cordes et logique tensorielle

Le cycle est composé de quatre séances, ouvertes à tous, qui se tiendront à l'Institut Galilée et au LIPN, avec le calendrier suivant :
  • 4 juillet 2011, 14h-16h, amphi Euler (Institut Galilée)
  • 7 juillet 2011, 10h-12h, salle B311 (LIPN)
  • 11 juillet 2011, 14h-16h, salle B311 (LIPN)
  • 13 juillet 2011, 14h-16h, salle B311 (LIPN)
LOVE 27/02/2019 On quantum complexity classes and quantum icc, par Margherita Zorzi
Margherita Zorzi  
B311
27/02/2019    15:22 -
Résumé :

Le 24 octobre 2011, à 14h en salle B311, le séminaire LCR accueille Margherita Zorzi (LIPN, post-doc ANR Complice).

One of the strong motivations behind quantum computing is computational complexity: quantum computers seem to be able to solve efficiently classical hard problems, thanks to the potential speed up in the execution time induced by superposition phenomena.

Quantum complexity theory has been developed since the Nineties, after the definition of quantum computational models such as quantum Turing machines and quantum circuit families. A particular attention is devoted to the quantum polytime classes (EQP, BQP, ZQP).

After a preliminarily discussion about quantum models and quantum complexity theory, the polytime quantum lambda calculus SQ (inspired by soft linear logic) is presented, showing an Implicit Computational Complexity approach in the quantum setting.

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

Le 16 janvier 2012, à 14h en salle B311, le séminaire LCR accueille Thomas Seiller (Chambéry).

Les graphes d'interaction généralisent la toute première géométrie de l'interaction définie par Girard dans l'article "Multiplicatives". En remplaçant les permutations (utilisées dans "Multiplicatives") par des graphes orientés pondérés, il est possible de définir une notion d'orthogonalité en comptant les cycles apparaissant lors du branchement de deux graphes. Il est alors possible d'obtenir une géométrie de l'interaction pour MALL dépendant de la fonction qui mesure les cycles.

Après avoir défini cette géométrie de l'interaction, je montrerai comment il est possible d'obtenir un modèle dénotationnel de MALL et une notion de vérité à partir de cette construction. Enfin, je montrerai qu'en choisissant judicieusement la fonction de mesure, il est possible d'obtenir soit la géométrie de l'interaction dans sa version ancienne (GdI1, avec une orthogonalité basée sur la nilpotence), soit une version combinatoire de la GdI5 de Girard. Ceci permet donc de donner une interprétation géométrique à l'orthogonalité de Girard basée sur le déterminant, et de relier cette nouvelle construction à celles plus anciennes basées sur la nilpotence.

LOVE 27/02/2019 Les stratégies pleinement paresseuses, par Thibaut Balabonski
Thibaut Balabonski  
B311
27/02/2019    15:22 -
Résumé :

Le 5 mars 2012, à 14h en salle B311, le séminaire LCR accueille Thibaut Balabonski (PPS).

Les stratégies de réduction avec partage fournissent des pistes pour l'évaluation efficace des programmes fonctionnels. En quarante ans, ces modes de réduction ont été définis dans des cadres formels variés, hétérogènes et parfois complexes, utilisant par exemple des clôtures, des graphes, ou des transformations de programmes.

Je présenterai un système de récriture simple et expressif dans lequel nombre de ces approches peuvent être unifiées, analysées, et comparées. On étudiera en particulier quelques avatars de la réduction pleinement paresseuse (dont une des variantes est implémentée dans le compilateur GHC) et on précisera en quoi ces différents systèmes sont équivalents. Enfin, une utilisation judicieuse d'une transformation de programmes classique (le lambda-lifting) permettra d'établir un lien entre la pleine paresse et la réduction optimale des systèmes du premier ordre.. Ce lien sera suffisamment fort pour permettre le transfert de propriétés non triviales du premier ordre vers le lambda-calcul.

LOVE 27/02/2019 A3: linear! dependent, par Arnaud Spiwack
Arnaud Spiwack  
B311
27/02/2019    15:22 -
Résumé :

Le 19 mars 2012, à 14h en salle B311, le séminaire LCR accueille Arnaud Spiwack (PiR2).

Herbelin & Curien's μ language gives a syntax to classical sequent calculus while leaving contraction and weakening implicit (more precisely dealt with by variables), like one would expect of a programming language. I will present an extension of H&C's μ for linear sequent calculus which still relies on variables for contraction and weakening. I will then proceed and show how to give it a hint of dependent types, though I must confess there are some troubles there.

LOVE 27/02/2019 Constructing differential categories and deconstructing categories of games, par Guy McCusker
Guy McCusker  
B311
27/02/2019    15:22 -
Résumé :

Le 12 mars 2012, à 14h en salle B311, le séminaire LCR accueille Guy McCusker (Université de Bath, invité LCR).

We present an abstract categorical construction of differential categories, that is categories suitable for modelling Ehrhard and Regnier's differential lambda calculus. We demonstrate that the relational model arises as an instance of our construction, as does a previously known category of games, exposing its differential nature that was not previously known. A new category of games is constructed in a similar way, and shown to be a fully complete model of a resource-sensitive version of PCF. The construction also gives us a collapse from the games model onto the relational model, which demonstrates that the relational model is fully abstract for resource PCF.

[Joint work with Jim Laird (Bath) and Giulio Manzonetto (LIPN, Paris 13)]

LOVE 27/02/2019 Introduction to triposes and intuitionistic realizability toposes, par Thomas Streicher
Thomas Streicher  
B311
27/02/2019    15:22 -
Résumé :

Le 19 mars 2012, à 13h30 en salle B311, le séminaire LCR accueille Thomas Streicher (Darmstadt).

A gentle introduction to the theory of triposes, intuitionistic realizability toposes, and the motivations behind them.

LOVE 27/02/2019 An imperative characterization of probabilistic polynomial time, par Paolo Parisen Toldin
Paolo Parisen Toldin  
B311
27/02/2019    15:22 -
Résumé :

Le 23 avril 2012, à 14h en salle B311, le séminaire LCR accueille Paolo Parisen Toldin (Bologne).

Contrary to ICC standard approach, we present a small WHILE language characterizing the class PP.

The main problem concerning the imperative approach is to understand how informations/values flow throw variables in a program.

In literature are well known many works that have polytime soundness but just few of them (using the imperative paradigm) are able to give a polytime completeness.

Our system, MAL0 (Multiplied, Affine, Linear, 0 dependeces ), is sound and complete. Moreover, our system can be used also to check if a program is running in probabilistic polytime (can be easily restrict to just polytime soundness). We claim that, contrary to works found in literature, our system is able to certify a program in polytime.

This is a joint work in progress with Jean-Yves Moyen.

LOVE 27/02/2019 Toward a bounded linear type system for pcf in call-By-value, par Barbara Petit
Barbara Petit  
B311
27/02/2019    15:22 -
Résumé :

Le 30 avril 2012, à 14h en salle B311, le séminaire LCR accueille Barbara Petit (Bologne).

 

LOVE 27/02/2019 Explicit substitutions at a distance, rewriting, and applications to the theory of lambda calculus, par Beniamino Accattoli
Beniamino Accattoli  
B311
27/02/2019    15:22 -
Résumé :

Le 14 mai 2012, à 14h en salle B311, le séminaire LCR accueille Beniamino Accattoli (LIX).

In some works in collaboration with Stefano Guerrini and Delia Kesner I developed a new approach to explicit substitutions, arising from Linear Logic proof-nets. The idea is to design calculi mimicking closely the dynamics of the graphical cut-elimination rules. Proof-nets and terms have very different notions of locality: this fact induce non-local, "at a distance" rewriting rules on terms. Substitution calculi at a distance are half-way lambda calculus and typical explicit substitution calculi: they retain most of the simplicity of lambda calculus, keeping the subtleties and the finer evaluation of explicit substitutions. In a series of recent works (some of which are joint works with Delia Kesner, Luca Paolini or Ugo Dal Lago) I explored systematically the rewriting theory of these calculi. In the talk I will survey the problems I studied (confluence, preservation of strong normalization, sigma-equivalence, developments, solvability, factorization, standardization, residuals) and the results I obtained, showing how they provide new understandings of classical notions and results - and sometimes even new results - in the theory of lambda-calculus.

LOVE 27/02/2019 The failure of the range property in the lambda theory h, par Andrew Polonsky
Andrew Polonsky  
B311
27/02/2019    15:22 -
Résumé :

Le 11 juin 2012, à 14h en salle B311, le séminaire LCR accueille Andrew Polonsky (Bergen).

We show that the lambda theory resulting from identification of all "meaningless" terms in the lambda calculus fails to satisfy the otherwise ubiquitous Range Property.  This is the condition that every term, seen via application as a map on closed terms, is either constant or has infinite range modulo identifications of the theory.  Specifically, we construct a term Xi such that in H one has for closed N:
Xi N = Xi I  <==>  Xi N =/= Xi Omega
The construction exposes certain pathological features of this
otherwise natural lambda theory.

LOVE 27/02/2019 Linearity in the non-Deterministic call-by-value setting, par Alejandro Di­az-Caro
Alejandro Di­az-Caro  
B311
27/02/2019    15:22 -
Résumé :

Le 7 juillet 2012, à 14h en salle B311, le séminaire LCR accueille Alejandro Di­az-Caro (LIPN).

We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting, which we will discuss in this presentation.

Joint work with Barbara Petit. To appear in LNCS ( Proceedings of WoLLIC'12 ). arXiv:1011.3542

LOVE 27/02/2019 Caractérisation de co-NL par l'action d'un groupe, par Clément Aubert
Clément Aubert, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 13:30
Résumé :
Girard, dans Normativity in Logic (2011), propose un emploi innovant de la Géométrie de l'Interaction (GdI) dans le facteur hyperfini pour caractériser des classes de complexité. Ce papier étant très technique et parfois allusif, nous proposons avec Thomas Seiller (LAMA - Université de Savoie) une relecture des résultats qu'il présente. En allégeant et simplifiant certaines définitions et critères, en introduisant un modèle de calcul innovant (les machines à pointeurs non-déterministes), nous parvenons à prouver de nouveau que co-NL peut être caractérisé par l'action du groupe des permutations finies sur une algèbre de von Neumann.
Un bagage minimum de Logique Linéaire et de complexité sont souhaitables pour comprendre les grandes lignes, nous n'entrerons pas dans le détail des preuves techniques concernant la GdI ou les algèbres de von Neumann, préférant renvoyer le lecteur intéressé (et patient !) vers notre papier (en anglais), disponible à http://lipn.fr/~aubert/article-coNL.pdf
LOVE 27/02/2019 Opérades et Surjections, par Muriel Livernet
Muriel Livernet, LAGA, Paris 13  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
Dans un premier temps j'expliquerai sur des exemples simples ce que sont les opérades. Dans un deuxième temps j'introduirai l'opérade des surjections et exposerai les questions combinatoires que l'on se pose afin de résoudre des problèmes en topologie algébrique.
LOVE 27/02/2019 Interaction Graphs and Complexity, par Thomas Seiller
Thomas Seiller, IHES  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
We obtained, with C. Aubert, new characterizations of complexity classes coNL and L using methods inspired from Girard's hyperfinite Geometry of Interaction (GoI). These characterizations had some drawbacks, among which:
- it used complicated tools from operator theory;
- it was not related to the interpretation of logic in the Geometry of Interaction construction;

This work revisits these previous results by using Interaction Graphs, a combinatorial GoI construction developed during my thesis that simplifies, unifies and generalizes Girard's GoI constructions. This change of perspective allows for a number of improvements, namely:
- the obtention of simplified characterizations of the classes coNL and L;
- the obtention of new characterizations, e.g. Regular languages, NL;
- it relates the method to the reconstruction of logic in Interaction Graphs (hence in GoI);
- it offers new ways to obtain characterizations of other classe.
LOVE 27/02/2019 On the computational meaning of axioms, par Mattia Petrolo
Mattia Petrolo, IHPST, Paris 1  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
An anti-realist theory of meaning suitable for both logical and proper axioms is investigated. As opposed to other anti-realist accounts, like Dummett-Prawitz verificationism, the standard framework of classical logic is not called into question. The reason being that semantical features are not limited solely to inferential ones, but also computational aspects are considered as essential in the process of determination of meaning. In order to deal with such computational aspects, a relaxation of syntax is shown to be necessary. This leads to the presentation of a general kind of proof theory, where the objects of study are not only typed objects like deductions, but untyped ones, where formulas have been replaced by geometrical configurations.

This is joint work with Alberto Naibo and Thomas Seiller
LOVE 27/02/2019 De la charactérisation des modèles de H*, par Flavien Breuvart
Flavien Breuvart, PPS/LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 11:30
Résumé :
Je donnerais une caractérisation (pour une large classe de model du lambda calcul pur) des modèles qui sont pleinement adéquat pour la normalisation de tête, càd dont la théorie est H*. Un K-model extentionel D est pleinement adéquat sii il est hyperimmune, càd que les comportements mal fondés ne sont pas capturées par aucun terme récursif.

LOVE 27/02/2019 Lambda-calculus and the Invariance Thesis, par Beniamino Accattoli
Beniamino Accattoli, Università di Bologna  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :

Slot and van Emde Boas’s invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is λ-calculus a reasonable ma- chine? Is there a way to measure the computational complexity of a λ-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based over a standard notion in the theory of λ-calculus: the invariant cost model is the length of a leftmost-outermost derivation to normal form. Such a theorem cannot be proved by directly relating λ-calculus with Turing machines or register machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponential output. The first step towards the solution is to shift to a notion of evaluation for which length and size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modelled after linear logic proof nets and that admits a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, register machines. The second step is to show that LSC is invariant with respect to the λ-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in the λ-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, deemed useful. Useful evaluation avoids those unsharing steps that only explicit the output without contributing to β-redexes, i.e. the steps that cause the blow-up in size. The main technical contribution of the paper is indeed the definition of useful reduction and the thorough analysis of their properties.

LOVE 27/02/2019 Paramétricité et type identité : application à la structure d'ω-groupoide des types, par Marc Lasson
Marc Lasson, PPS - PiR2  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
La paramétricité est un concept introduit par Reynolds afin d'étudier
l'abstraction de type polymorphe du système F. Elle renvoie au
fait que des programmes bien typés ne peuvent ``inspecter le type de leurs
arguments'': ils doivent se comporter uniformément au regard des
types abstraits. Reynolds formalise cette notion en montrant que les
programmes polymorphes du système F satisfont des relations
logiques définies par induction sur la structure des types. Le système de
types sous-jacent à coq est suffisamment expressif pour exprimer
sa propre théorie de la paramétricité. Dans cet exposé, nous nous
intéresserons aux conséquences de cette remarque lorsqu'elle est
appliquée au type des égalités, et nous montrerons en particulier comment
montrer des résultats de paramétricité concernant les espaces de lacet
(loop spaces, en anglais) et en déduire des résultats sur la structure de
groupoide de la théorie des types.
LOVE 27/02/2019 Two Intensional Phenomena: The Size of Church-Rosser Diagrams, and Characterization of PTIME via Overlapping Cons-Free Systems, par Jakob Grue Simonsen
Jakob Grue Simonsen, Datalogisk Institut, Copenhague  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
We will informally discuss two very different problems that both concern the intensional behaviour of very simple calculi: First-order term rewriting systems, respectively lambda calculus.

The first problem concerns finding bounds on the size of confluence and Church-Rosser diagrams: If s is a term in a confluent, we know that every "peak" t *<-s ->* t' has a corresponding "valley" t ->* s' *<- t', but it is not at all clear how the number of steps in the "valley" relates
to the number of steps in the "peak" and to the size of the starting term s. We will discuss how valley sizes can always be computed, how
the sizes may majorize any computable function on the integers, how exponential bounds can be found for first-order term rewriting, and
for lambda calculus how there is an enormous difference between the best-known upper bound (not even elementary recursive) and the worst-case example known (doubly exponential).

The second problem concerns implicit complexity and how to characterize the set of PTIME-decidable sets by first-order term rewriting systems
in the most liberal fashion possible: No restrictions on reduction strategy (hence no insistence on call-by-name, call-by-value or other
functional-programming-inspired strategies), no restrictions on overlaps between left-hand sides of rules, and as few linearity constraints as we can get away with (and absolutely no explicit typing of any kind).

The talk will be kept at high-level and present the interesting problems and challenges; we will only delve into technical details if the audience feels like it. The material presented is based on joint, ongoing, work with Jeroen Ketema and Daniel de Carvalho.
LOVE 27/02/2019 Ludique et types: éléments de déconstruction, par Christophe Fouqueré
Christophe Fouqueré, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
We will discuss/analyze the following observations and the questions they rise:

Observations:
- Each formula of MALL2 is denoted by a behaviour in Ludics.
- Cut-elimination is fully plugged into / at the heart of Ludics.
- And with properties expected for a logic.

Questions:
- Can we characterize exactly behaviours that denote MALL(c/2/inf) formulas?
- Can we define the algebraic structure of a behaviour? I.e. a language for behaviours?
- Can we develop a sequent calculus for this language?
LOVE 27/02/2019 Behavior driven design for tests and verification, par Ulrich Kühne
Ulrich Kühne, University of Bremen  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
In the course of an exploratory project on hardware and system design and verification, we are looking for new ways how to bridge the gap between early abstract models and later implementation phases. One possible approach is the adaptation of agile techniques to the hardware domain, enhanced by model checking techniques. While in the design of hardware systems, testing and verification are usually applied as a post-process, software developement is pushed towards agile techniques like Test Driven Development (TDD), where tests play a central role.  Behavior driven development (BDD) extends TDD as a well established software development technique. Essentially, in both techniques testing and implementing is interleaved, with the test cases being written first. In BDD, test cases are written in natural language which enables the discussion with stakeholders and easy requirements tracking throughout the design. In this talk, I will present a BDD tool for the Verilog hardware design language, which extends BDD with formal techniques. From test cases, properties can be generalized, making the verification more reliable, without the need to manually specify temporal properties.
LOVE 27/02/2019 Can Dialectica break bricks?, par Pierre-Marie Pédrot
Pierre-Marie Pédrot, PPS, Université Paris 7  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :

The Dialectica translation is a logical transformation described by Gödel in 1958, but designed in the 30's. At the end of the 80's, it was given a categorical counterpart, which happened to be compatible with the usual decomposition of intuitionistic logic into linear logic. Still, it was lacking a true Curry-Howard interpretation.

We will fill this hole by presenting the computational content of Dialectica by means of an untyped lambda-calculus translation. We will show that this translation has a really simple explanation as soon as we put our source term in the Krivine abstract machine, except for a disturbing detail, seemingly deeply rooted in linear logic. We will also show how our presentation can be naturally applied to a dependently-typed system almost without adaptation, thus giving a hindsight on how linear dependent types may be built (or not).

LOVE 27/02/2019 Data-race freedom by typing in Mezzo, par Thibaut Balabonski
Thibaut Balabonski, INRIA  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 11:30
Résumé :
Mezzo is a typed programming language in the ML family whose static discipline controls aliasing and ownership. This rules out certain mistakes, including representation exposure and data races, and opens up new opportunities, such as gradual initialization or (more generally, and somewhat speculatively) the definition and enforcement of object protocols.

In this talk, I will explain the basic design of Mezzo on examples, and show how its type system inspired by separation logic gives a simple way of tracking ownership of fragments of shared memory between concurrent threads. Beyond the usual claim that "well-typed programs do not go wrong", we guarantee that well-typed Mezzo programs have no data-races.

LOVE 27/02/2019 Quelques remarques d'ordre logique sur la théorie des types homotopiques (1ère partie), par Christophe Fouqueré
Christophe Fouqueré, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
A partir du livre "Homotopy Type Theory", seront abordés les points suivants: théorie des types (à la Martin-Löf), notions (très) élémentaires d'homotopie et axiome d'univalence, hiérarchisation des types et conséquences sur la partie interprétant la logique (en particulier le tiers-exclus). Nous n'aborderons pas nombre de points (théorie des catégories, types homotopiques d'ordre supérieur, reconstruction des réels, ...) hautement intéressants de ce livre.
LOVE 27/02/2019 Présentation de l2coq : une bibliothèque pour des preuves linéaires en Coq, par Micaela Mayero
Micaela Mayero, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
Dans cette séance je présenterai l2coq, développé par O. Laurent et D. Pous. Il s'agit d'un "sous-ensemble de Coq" (sous la forme d'une bibliothèque "restrictive") permettant de faire des preuves de propriétés linéaires (ILL, ELL, LLL, SLL). Olivier en avait fait une présentation le jour de la soutenance d'HDR de Virgile. En 1 an, l2coq a continué d'évoluer. Je vous propose de revenir sur les bases de l2coq en vous montrant également le code et j'expliquerai pourquoi j'ai mis quelques mots entre guillemet dans les phrases précédentes. Pour cela, je ferai des rappels (ou pas pour certains) de la théorie de Coq en me basant sur l'exposé précédent de Christophe, la partie théorie des types. Vers la fin ou en cours d'exposé, je vous ferai une démo, durant laquelle nous pourrons tenter ensemble de faire des preuves formelles de propriétés linéaires (ILL dans un premier temps).
LOVE 27/02/2019 Quelques remarques d'ordre logique sur la théorie des types homotopiques (2e partie), par Christophe Fouqueré
Christophe Fouqueré, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 13:30
Résumé :
A partir du livre "Homotopy Type Theory", seront abordés les points suivants: théorie des types (à la Martin-Löf), notions (très) élémentaires d'homotopie et axiome d'univalence, hiérarchisation des types et conséquences sur la partie interprétant la logique (en particulier le tiers-exclus). Nous n'aborderons pas nombre de points (théorie des catégories, types homotopiques d'ordre supérieur, reconstruction des réels, ...) hautement intéressants de ce livre.
LOVE 27/02/2019 Models of a Non-Associative Composition, par Guillaume Munch-Maccagnoni
Guillaume Munch-Maccagnoni, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
We characterise the polarised evaluation order through a categorical structure where the hypothesis that composition is associative is relaxed. Duploid is the name of the structure, as a reference to Jean-Louis Loday's duplicial algebras. The main result is a reflection Adj→Dupl where Dupl is a category of duploids and duploid functors, and Adj is the category of adjunctions and pseudo maps of adjunctions. The result suggests that the various biases in denotational semantics: indirect, call-by-value, call-by-name... are a way of hiding the fact that composition is not always associative.
LOVE 27/02/2019 Proving complexity bounds in linear logic with context semantics, par Matthieu Perrinel
Matthieu Perrinel, ENS Lyon  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
First, I will present a simplified version of Ugo Dal Lago's context
semantics on proof-nets. Next, I will present abstract properties based on
context semantics which entail complexity bounds. I will use this
properties to make short proofs of strong complexity bounds for ELL and
LLL. Finally, I will sketch how we are currently using context semantics to
give new type systems characterizing Ptime and the first LL-based type
system characterizing primitive recursive functions.
LOVE 27/02/2019 Intensionnalité vs. extensionnalité : où est-elle la frontière ? (3e partie), par Jean-Yves Moyen
Jean-Yves Moyen, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
Au cours de ces trois séances de groupe de travail, je ferai le "débriefing" de mon CRCT et je vous présenterai les résultats obtenus à Nancy en collaboration avec Guillaume Bonfante et Pierre, ou à Copenhague en collaboration avec James Avery et Jakob Simonsen (qui sera par ailleurs prof invité chez nous en février).

Au gré de vos interruptions et de nos discussions, nous parlerons sans doute de Rice et de Gödel, de cardinaux et de grands ordinaux, d'ordre supérieur et de non déterminisme, de treillis, de partitions, peut-être de topologie. Les catégoriciens pourront s'exercer à faire commuter des diagrammes. Ne reniant pas mes origines, tout cela sera enrobé dans une couche de complexité implicite.


Le point de départ est une relecture du théorème de Rice entamée avec Pierre il y a quelques années. Au lieu de parler de "propriétés extensionnelles", le résultat est vu comme parlant de l'équivalence extensionnelle (p et q sont équivalents si ils calculent la même fonction). Autrement dit, on quotiente l'ensemble des programmes par leur extension.

Cette vision fait de Rice une équivalence parmi d'autres et on peut chercher d'autres équivalences "intéressantes" entre programmes. Notamment, l'ensemble des équivalences formant un treillis complet, on peut étudier ce treillis.
LOVE 27/02/2019 Intensionnalité vs. extensionnalité : où est-elle la frontière ? (2e partie), par Jean-Yves Moyen
Jean-Yves Moyen, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
Au cours de ces trois séances de groupe de travail, je ferai le "débriefing" de mon CRCT et je vous présenterai les résultats obtenus à Nancy en collaboration avec Guillaume Bonfante et Pierre, ou à Copenhague en collaboration avec James Avery et Jakob Simonsen (qui sera par ailleurs prof invité chez nous en février).

Au gré de vos interruptions et de nos discussions, nous parlerons sans doute de Rice et de Gödel, de cardinaux et de grands ordinaux, d'ordre supérieur et de non déterminisme, de treillis, de partitions, peut-être de topologie. Les catégoriciens pourront s'exercer à faire commuter des diagrammes. Ne reniant pas mes origines, tout cela sera enrobé dans une couche de complexité implicite.


Le point de départ est une relecture du théorème de Rice entamée avec Pierre il y a quelques années. Au lieu de parler de "propriétés extensionnelles", le résultat est vu comme parlant de l'équivalence extensionnelle (p et q sont équivalents si ils calculent la même fonction). Autrement dit, on quotiente l'ensemble des programmes par leur extension.

Cette vision fait de Rice une équivalence parmi d'autres et on peut chercher d'autres équivalences "intéressantes" entre programmes. Notamment, l'ensemble des équivalences formant un treillis complet, on peut étudier ce treillis.
LOVE 27/02/2019 Intensionnalité vs. extensionnalité : où est-elle la frontière ? (1ère partie), par Jean-Yves Moyen
Jean-Yves Moyen, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
Au cours de ces trois séances de groupe de travail, je ferai le "débriefing" de mon CRCT et je vous présenterai les résultats obtenus à Nancy en collaboration avec Guillaume Bonfante et Pierre, ou à Copenhague en collaboration avec James Avery et Jakob Simonsen (qui sera par ailleurs prof invité chez nous en février).

Au gré de vos interruptions et de nos discussions, nous parlerons sans doute de Rice et de Gödel, de cardinaux et de grands ordinaux, d'ordre supérieur et de non déterminisme, de treillis, de partitions, peut-être de topologie. Les catégoriciens pourront s'exercer à faire commuter des diagrammes. Ne reniant pas mes origines, tout cela sera enrobé dans une couche de complexité implicite.


Le point de départ est une relecture du théorème de Rice entamée avec Pierre il y a quelques années. Au lieu de parler de "propriétés extensionnelles", le résultat est vu comme parlant de l'équivalence extensionnelle (p et q sont équivalents si ils calculent la même fonction). Autrement dit, on quotiente l'ensemble des programmes par leur extension.

Cette vision fait de Rice une équivalence parmi d'autres et on peut chercher d'autres équivalences "intéressantes" entre programmes. Notamment, l'ensemble des équivalences formant un treillis complet, on peut étudier ce treillis.
LOVE 27/02/2019 Bisimulations from graphical encodings (DPOs, RPOs, cospans, and all that), par Fabio Gadducci
Fabio Gadducci, Università di Pisa  
Amphi Copernic, Institut Galilée, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
The talk presents a personal recollection of recent results on the synthesis of labelled transition systems (LTSs) for process calculi. 
The starting point is a visual technique for modelling the reduction semantics of nominal calculi: processes are mapped into graphs equipped with "interfaces", such that the denotation is fully abstract with respect to the structural congruence. The encoding allows for the reuse of standard graph rewriting theory and tools for simulating the reduction semantics of the calculus, such as the "double pushout" (DPO) approach and its concurrent semantics (which allows for the simultaneous execution of independent reductions)
Graphs with interfaces are just an instance of a cospan category (over the category of graphs). which is amenable to the synthesis mechanism based on "borrowed contexts" (BCs), proposed by Ehrig and Koenig, which are in turn an instance of "relative push outs" (RPOs), originally introduced by Milner and Leifer. The BC mechanism allows for the effective construction of an LTS that has graphs with interfaces as both states and labels, and such that the associated bisimilarity is automatically a congruence. 
Since the category of cospans over graphs admits RPOs (as proved by Sassone and Sobocinski), its choice as the domain of the encoding for nominal calculi ensures that the synthesis of an LTS can be performed, and that a compositional observational equivalence is obtained. The talk discusses the LTS distilled by exploiting the encoding of CCS and Mobile Ambients processes.
LOVE 27/02/2019 From Mind to Turing to Mind, par Henk Barendregt
Henk Barendregt, Radboud University Nijmegen  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 13:30
Résumé :
Based on introspection Alan Turing analyzed the process by which humans perform  computations. Recent papers on consciousness go in the other direction: this is seen as a hybrid Turing machine process. Hybrid in the sense that it acts both discretely and in parallel, where the Turing machine quadruplets are implemented by a neural net.

We also focus on mind-states and their possible implementations in the brain, based on recent progress in neuroscience.

If the claims in the talk are validated one day, then this would be emperical evidence for the Church-Turing thesis
LOVE 27/02/2019 Graphical Foundations for Dialogue Games, par Cai Wingfield
Cai Wingfield, University of Bath  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 14:00
Résumé :
In 2007, Harmer, Hyland and Melliès gave a formal mathematical foundation for game semantics using a notion they called a schedule, a structure describing interleavings of plays in games.  Their definition was combinatorial in nature, but researchers often draw pictures when describing schedules in practice.  Moreover, several proofs of key properties, such as that the composition of schedules is associative, involve cumbersome combinatorial detail, whereas in terms of pictures the proofs are straightforward, reflecting the geometry of the plane.  Here, we give a geometric formulation of schedules, prove that they are isomorphic to Harmer et al.'s definitions, and illustrate their value by giving such geometric proofs.  Harmer et al.'s notions may be combined to describe plays in multi-component games, and researchers have similarly developed intuitive graphical representations of plays in these games.  We give a characterisation of these diagrams and explicitly describe how they relate to the underlying schedules, finally using this relation to provide new, intuitive proofs of key categorical properties.

This is a joint work with Guy McCusker and John Power.

LOVE 27/02/2019 Forcing in classical realizability: the case study of Herbrand trees, par Lionel Rieg
Lionel Rieg, ENS Lyon  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 14:30
Résumé :
Krivine presented in 2010 a methodology to combine Cohen's forcing with the theory of classical realizability and showed that the forcing condition can be seen as a reference that is not subject to backtracks. The underlying classical program transformation was then analyzed by Miquel (2011) in a fully typed setting in classical higher-order arithmetic (PAw+).

As a case study of this methodology, I present a method to extract a Herbrand tree from a classical realizer of an existential formula, following the idea of the proof of Herbrand theorem.  Unlike the traditional proof based on Konig's lemma (using a fixed enumeration of atomic formulas), our method is based on the introduction of a particular Cohen real.  It is formalized as a proof in PAw+, making explicit the construction of generic sets in this framework in the particular case where the set of forcing conditions is arithmetical.  We then analyze the algorithmic content of this proof.
LOVE 27/02/2019 Some Results for Linear Logic Full Completeness, par Hugh Steele
Hugh Steele, IML, Aix-Marseille  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 14:00
Résumé :
Many full completeness theorems have been established for fragments of
linear logic since the notion was first defined by Samson Abramsky and
Radha Jagadeesan in their 1992 paper. For the most part, these results
are obtained on a case-by-case basis: the subject of each proof is
precisely one category.

In this talk it is shown that the Hyland-Tan double glueing
construction can transform all tensor-generated compact closed
categories with finite biproducts into fully complete models of
unit-free MLL. The arguments employed are based around considering the
combinatorics behind the construction using standard linear algebra.
It is also discussed how another double glueing construction may be
able to create similar categories satisfying unit-free MALL full
completeness.
LOVE 27/02/2019 Hypercoherence Spaces form a double-glued Category , par Hugh Steele
Hugh Steele, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
Ehrhard's Hypercoherence Spaces proved a useful medium through which to study strongly stable semantics. The category of hypercoherence spaces (HypCoh) has also been shown to be the bedrock of one of the very few fully complete models of unit-free multiplicative additive linear logic, satisfying Joyal's softness condition. Much like in the category of coherence spaces (Coh), an object of HypCoh is a set equipped with a collection of its subsets, with morphisms being relations respecting restrictions set by these `cliques'. However, unlike Coh, HypCoh has not been formalised as a true double-glued category.

In this talk I show that HypCoh is indeed such a category (if you're willing to bend the rules a little!). We also see how far the spirit of the glueing construction may be generalised to produce categories with similar properties.
LOVE 27/02/2019 Are partial orderings intrinsic to computations?, par Antonino Salibra
Antonino Salibra, Università Ca' Foscari Venezia  
Salle à fixer, Université de Villetaneuse
27/02/2019    15:22 - 13:30
Résumé :
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda terms, the so-called subtractive equations, consistent with lambda calculus but not contemporaneously satisfied in any Scott continuous model. We also relate the subtractive equations to the open problem of the order-incompleteness of lambda calculus, by studying the connection between the notion of absolute unorderability in a specific point and a weaker notion of subtractivity, namely n-subtractivity, for partially ordered algebras. Finally we study the relation between n-subtractivity and relativized separation conditions in topological algebras, obtaining an incompleteness theorem for a general topological semantics of lambda calculus.
LOVE 27/02/2019 Some Results for Linear Logic Full Completeness, par Hugh Steele
Hugh Steele, IML, Aix-Marseille  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 13:30
Résumé :
Many full completeness theorems have been established for fragments of
linear logic since the notion was first defined by Samson Abramsky and
Radha Jagadeesan in their 1992 paper. For the most part, these results
are obtained on a case-by-case basis: the subject of each proof is
precisely one category.

In this talk it is shown that the Hyland-Tan double glueing
construction can transform all tensor-generated compact closed
categories with finite biproducts into fully complete models of
unit-free MLL. The arguments employed are based around considering the
combinatorics behind the construction using standard linear algebra.
It is also discussed how another double glueing construction may be
able to create similar categories satisfying unit-free MALL full
completeness.
LOVE 27/02/2019 On type isomorphisms in simultaneous presence of sums and functions, par Danko Ilik
Danko Ilik, LIX, Ecole polytechnique  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
We consider the problem of characterizing isomorphisms of types, or, equivalently, constructive cardinality of sets, in the simultaneous presence of disjoint unions, Cartesian products, and exponentials. Mostly relying on results about polynomials with exponentiation that have not been used in our context, we derive: that the usual finite axiomatization known as High-School Identities (HSI) is complete for a significant subclass of types; that it is decidable for that subclass when two types are isomorphic; that, for the whole of the set of types, a recursive extension of the axioms of HSI exists that is complete; and that, for the whole of the set of types, the question as to whether two types are isomorphic is decidable when base types are to be interpreted as finite sets. We also point out certain related open problems.
LOVE 27/02/2019 A Core Quantitative Coeffect Calculus, par Aloïs Brunel
Aloïs Brunel, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:15
Résumé :
Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this talk, we present a language, called lRPCF, inspired by a generalized interpretation of the exponential modality of bounded linear logic. In lRPCF exponential modalities carry a label--an element of a semiring--providing additional information on how a program uses its context. This additional information is used to express comonadic type analysis.
LOVE 27/02/2019 Game semantics and applications to compilation (1/3): Semantic foundations of heterogeneous compilation, par Dan Ghica
Dan Ghica, University of Birmingham  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 15:30
Résumé :
This is an introductory, motivational and methodological talk in which I will describe my "Seamless Computing" research programme. By "seamless" I mean that programming languages for unconventional architectures (e.g. distributed, reconfigurable, heterogeneous) can still conform to the long-established principles of machine independence, recast in this new setting. I will talk about when and how such conventional languages (higher-order, imperative, concurrent) can be compiled in a seamless way, using ideas based on the Geometry of Interaction and on game semantics.
LOVE 27/02/2019 Game semantics and applications to compilation (2/3): Abstract machines for game semantics, par Dan Ghica
Dan Ghica, University of Birmingham  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 15:30
Résumé :
We will examine new abstract machines for game semantics which correspond to networks of conventional computers, and which can be used as an intermediate representation for distributed compilation. This is achieved in two steps. First we introduce the HRAM, a Heap and Register Abstract Machine, an abstraction of a conventional computer, which can be structured into HRAM nets, an abstract point-to-point network model. HRAMs are multi-threaded and subsume communication by tokens (cf. IAM) or jumps (cf. JAM). Game Abstract Machines (GAM), are HRAMs with additional structure at the interface level, but no special operational capabilities. We show that GAMs cannot be naively composed, but composition must be mediated using special HRAM combinators. HRAMs are flexible enough to allow the representation of game models for languages with state (non-innocent games) or concurrency (non-alternating games). We illustrate the potential of this technique by implementing a toy distributed compiler for ICA, a higher-order programming language with shared state concurrency, thus significantly extending our previous distributed PCF compiler. We show that compilation is sound and memory-safe, i.e. no (distributed or local) garbage collection is necessary. [Joint work with Olle Fredriksson, to appear at LICS'13]
LOVE 27/02/2019 Vers une meilleur compréhension de l'adéquation complète, par Flavien Breuvart
Flavien Breuvart, Paris 7 (PPS)  
Salle A303, LIPN
27/02/2019    15:22 - 14:30
Résumé :
L'adéquation complète est une propriété liant un modèle dénotationnel et
une syntaxe qui assure une identité entre l’équivalence observationnel et
l'équivalence dénotationnel. Deux programmes sont dits
observationnellement équivalents s'ils se comportent à l’identique quelque
soit le contexte (cf bisimulations) et sont dits dénotationnellement
équivalent s'ils ont la même interprétation dans le modèle.
Nous allons alors regarder de plus près cette propriété pour se rendre
compte qu'elle implique généralement des preuves non triviales. Puis nous
étudierons les différentes techniques de preuves de la littérature. Et
enfin, partant d'une technique de preuve original, nous essayerons
d'établir une caractérisation de l'adéquation complète dans le cas
particulier du lambda-calcul et des modèles de Krivines (ou des modèles de
filtres ou encore des typages avec intersection).
LOVE 27/02/2019 Linear Dependent Types For Differential Privacy, par Marco Gaboardi
Marco Gaboardi, University of Pennsylvania / Università di Bologna  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 14:30
Résumé :
Differential privacy offers a way to answer queries about
sensitive information while offering strong, provable privacy guarantees.
 Several tools have been developed for certifying that a given query is
differentially private. In one approach, Reed and Pierce[31] proposed a
functional programming language, Fuzz, for writing differentially private
queries. Fuzz uses linear types to track sensitivity, as well as a
probability monad to express randomized computation; it guarantees that any
program that has a certain type is differentially private. Fuzz can
successfully verify many useful queries. However, it fails when the
analysis depends on values that are not known statically.
We present DFuzz, an extension of Fuzz with a combination of linear indexed
types and lightweight dependent types. This combination allows a richer
sensitivity analysis that is able to analyze a larger class of queries,
including queries whose sensitivity depends on runtime information. As in
Fuzz, the differential privacy guarantees follows directly from the
soundness theorem for the type system. We demonstrate the enhanced
expressivity of DFuzz by certifying differential privacy a broad class of
iterative algorithms that could not be typed previously. We conclude by
discussing the challenges of DFuzz type checking.
LOVE 27/02/2019 Unification and Logarithmic space , par Marc Bagnol
Marc Bagnol, IML, Université Aix-Marseille  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
I will present an algebraic characterization of the complexity
classes Logspace and NLogspace, using an algebra with a composition
law based on unification. This bridge between unification and
complexity classes is inspired from proof theory and more specifically
linear logic and Geometry of Interaction.
LOVE 27/02/2019 Unfolding-based Reachability Checking of Petri Nets, par César Rodríguez
César Rodríguez, LCR  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 17:00
Résumé :
In model checking, a well known source of state-space explosion (SSE) is the explicit representation of concurrent actions by their interleavings. Partial-order reductions attempt to address this by constructing an equivalent state space where irrelevant executions of the original are discarded. A comparatively less well-known approach emerges from the use of partial-order semantics, where the state space is instead represented by a partial order where concurrent actions are simply left unordered. Petri net unfoldings are arguably the most prominent verification technique issued from this idea. In this talk, three different semantics for Petri nets will be presented, the last one of which will be the aforementioned unfolding semantics. We will then see how unfoldings can be employed in practical verification and, time permitting, how to improve the method to address additional sources of SSE.
LOVE 27/02/2019 Asynchronous Interaction with Theorem Provers: ProofGeneral's Last March, par Carst Tankink
Carst Tankink, Inria Saclay  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:30
Résumé :
This year ProofGeneral, the generic Emacs-interface for proof assistants, celebrates its 20th birthday. The tool is showing its age, however, by only allowing a user to work at a single point at the time, and having to re-evaluate an entire proof script in reaction to changes at the beginning. In this talk, I will discuss our recent efforts to changing this situation: based on a previous endeavour in Isabelle, we have adapted the Coq proof assistant to work with the jEdit text editor. This editor has no user-visible notion of "State": the entire proof is always available to the proof assistant, allowing it to react to changes in the document in a more intelligent manner: by scheduling proofs in parallel and by postponing computation that are of no direct interest to the author. I will not go into full technical details in this talk, but give a demo of the current prototype, and discuss the ramifications of such a model in the longer term.
LOVE 27/02/2019 Construction de l'exponentielle libre en logique linéaire, par Luc Pellissier
Luc Pellissier, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:30
Résumé :
Groupe de travail sur une extension des méthodes introduites par Paul-André Melliès et Nicolas Tabareau pour calculer le comonoïde commutatif libre dans une catégorie avec produits (c.-à-d. un modèle de la logique linéaire multiplicative additive). On introduira les concepts nécessaires (PROPs, extensions de Kan, fins, etc.) et on expliquera sous quelles conditions on peut donner une formule close pour le calcul du comonoïde commutatif libre. On verra que ces conditions sont vérifiées dans tous les modèles connus de la logique linéaire, alors que les conditions originalement proposées par Melliès et Tabareau ne sont pas vérifiées par le modèle des espaces de finitude.
LOVE 27/02/2019 The implementation of GPGPU for Model Checking Problems, par WU Zhimin
WU Zhimin, Nanyang Technological University, Singapore  
Salle A303
27/02/2019    15:22 - 16:30
Résumé :
In this presentation, I will introduce the implementation of GPGPU techniques in model checking area. I target Nvidia GPU so firstly, the latest CUDA Compute Architecture will be introduced, together with the key points of GPU Program optimization. Then I will refer to some existing research on GPU accelerated Model Checking Problems. Finally, I will briefly introduce my research work. (This will be an informal presentation.)
LOVE 27/02/2019 Modèles et paradigmes de programmation parallèle distribuée, par Camille Coti
Camille Coti, AOC, LIPN, Paris 13  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 16:30
Résumé :
Dans cette présentation, qui sera plus un panorama qu'un séminaire de recherche, je présenterai quelques grands paradigmes de programmation parallèle distribuée à travers les modèles de mémoire distribuée et de communications inter-processus. Le but de mon exposé sera de présenter comment le caractère distribué des données est représenté et manipulé dans ces paradigmes de programmation afin de réfléchir à quelles techniques de programmation adopter selon les patterns d'accès aux données d'un programme séquentiel que l'on souhaite paralléliser. Je mettrai l'accent sur la mémoire distribuée, la mémoire partagée distribuée, les sacs de tâches, les communications implicites unilatérales et bilatérales, la parallélisation automatique par compilation.
LOVE 27/02/2019 Introduction to Partial Order Reductions , par César Rodríguez
César Rodríguez, LCR, LIPN, Paris 13  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 17:00
Résumé :
In model checking, a well known source of state-space explosion (SSE) is the explicit representation of concurrent actions by their interleavings. Partial-order reductions (PORs) are a family of techniques attempting to cope with this by constructing an equivalent state space where irrelevant executions of the original are discarded. This talk will be a gentle introduction to the topic. We will focus on Godefroid's persistent sets, prove that a selective exploration based on them visits all deadlocks, discuss the two main classes of algorithms for computing them, and finish, time permitting, with an overview of the conceptual similarities and differences between PORs and the unfolding technique.
LOVE 27/02/2019 Approche philologique des langages de programmation, par Baptiste Mélès
Baptiste Mélès, Archives Poincaré  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:30
Résumé :
La théorie des langages de programmation s'appuie généralement sur des langages de programmation théoriques — lambda-calcul, machines de Turing, et leurs variantes — que l'on suppose représenter fidèlement — à compilation près ! — les propriétés des langages de programmation de la « vraie vie », si l'on entend par là ceux que les programmeurs utilisent pour écrire des programmes utiles au quotidien : C, C++, Perl, etc. Or nous allons voir que les langages de programmation de la vraie vie possèdent bien des propriétés dont nul ne voudrait dans un langage théorique, et que la compilation écrase : des commandes inutiles, des redondances, des résidus purement historiques... Qui plus est, loin d'être un fait simplement négatif, ces propriétés constituent une bonne part de leur expressivité du point de vue du programmeur, et sont autant de points communs avec les langues naturelles. Nous verrons ainsi que des outils linguistiques et philologiques peuvent être mobilisés pour décrire une « sémantique du programmeur », qui échappe pour une bonne part aussi bien aux sémantiques courantes des langages de programmation qu'aux tentatives de description formelle de l'expressivité des langages de programmation.
LOVE 27/02/2019 New applications of moment-SOS hierarchies, par Victor Magron
Victor Magron, Imperial College London  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:30
Résumé :
Semidefinite programming is relevant to a wide range of mathematic fields, including combinatorial optimization, control theory, matrix completion. In 2001, Lasserre introduced a hierarchy of semidefinite relaxations for particular polynomial instances of the Generalized Moment Problem (GMP). My talk emphasizes new applications of this moment-SOS hierarchy, investigated during my PhD and Postdoc research. In the context of formal proofs for nonlinear optimization, one can combine the moment-SOS hierarchy with maxplus approximation of semiconvex functions. Such a framework is mandatory for formal certification of nonlinear inequalities, occurring by thousands in the proof of Kepler Conjecture by Hales. I also present how to approximate, as closely as desired, the Pareto curve associated with bicriteria polynomial optimization problems or the projections of semialgebraic sets. For each problem, one builds a hierarchy of semidefinite programs, so that the sequence of bounds converges in L1 norm. Finally, this hierarchy allows to analyze programs containing loop invariants with polynomial assignments.
LOVE 27/02/2019 Chemins en ludique non-linéaire, par Alice Pavaux
Alice Pavaux, LIPN  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 12:00
Résumé :
La ludique est une théorie logique basée sur l'interaction, introduite il y a une quinzaine d'années par J.-Y. Girard. Elle s'inscrit dans un contexte marqué par les avancées importantes en théorie de la démonstration et en sémantique des langages de programmation permises par la logique linéaire. On se propose ici d'étudier les mécanismes de l'interaction dans une variante non-linéaire de la ludique, afin de poser les outils nécessaires à l'étude des types dans ce cadre. Cela se fera en décrivant les chemins suivis au cours de l'interaction au sein des desseins, les objets de la ludique. La non-linéarité permet de ne pas se restreindre au fragment multiplicatif-additif de la logique linéaire.
LOVE 27/02/2019 Abstraction and Modular Verification of Services Using Symbolic Observation Graph (SOG), par Hanene Ochi
Hanene Ochi, LCR, LIPN, Paris 13  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 16:30
Résumé :
For automatically composing services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) without including any additional information that can be used to disclose the privacy of these services. The compatibility between two services can be based either on some generic properties or specific ones . This talk will present my work during my thesis about the problem considering these kinds of compatibility criteria, and we will introduce approches for the automatic abstraction of services and to the modular checking of their compatibility using their abstract models only. To abstract services, we use the symbolic observation graph (SOG) approach that preserves necessary informa tion for service composition and hides private information. We will show how the SOG can be adapted and used so that the verification of generic and specific compatibility criteria can be performed on the composition of the abstract models of services instead of the original composite service.
LOVE 27/02/2019 Precise Robustness Analysis of Real-Time Systems, par Étienne André
Étienne André, LCR, LIPN, Paris 13  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 17:00
Résumé :
Quantifying the robustness of a real-time system consists in measuring the maximum extension of the timing delays such that the system still satisfies its specification. In this work, we introduce a more precise notion of robustness, measuring the allowed variability of the timing delays in their neighbourhood. We consider here the formalism of time Petri nets extended with inhibitor arcs. We use the inverse method, initially defined for timed automata. Its output, in the form of a parametric linear constraint relating all timing delays, allows the designer to characterise the system local robustness, and hence to identify the delays allowing the least variability. We also exhibit a condition and a construction for rendering robust a non-robust system. This work is a joint work with Laure Petrucci.
LOVE 27/02/2019 CosyVerif: An Open Source Extensible Verification Environment, par Étienne André
Étienne André, LCR, LIPN, Paris 13  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 17:00
Résumé :
Over the past two decades, numerous verification tools have been successfully used for verifying complex concurrent systems, modelled using various formalisms. However, it is still hard to coordinate these tools since they rely on such a large number of formalisms. Having a proper syntactical mechanism to interrelate them through variability would increase the capability of eff ective integrated formal methods. Here, we propose a modular approach for defining new formalisms by reusing existing ones and adding new features and/or constraints. Our approach relies on standard XML technologies; their use provides the capability of rapidly and automatically obtaining tools for representing and validating models. It thus enables fast iterations in developing and testing complex formalisms. As a case study, we applied our modular definition approach on families of Petri nets and timed automata. This work is implemented in the CosyVerif platform, a modular framework integrating verification software tools of the Paris regions. This is a joint work with the CosyVerif team.
LOVE 27/02/2019 Teaching Formal Methods: Experience at UPMC and UP13 with CosyVerif, par Laure Petrucci
Laure Petrucci, LCR, LIPN, Paris 13  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 17:00
Résumé :
Nowadays, students are more and more demanding for practical coursework, which is a challenge when teaching formal approaches to software engineering. The solution is to provide environments for such hands-on sessions and homework, but this raises numerous difficulties. The environment must be: (i) multi-platform (Mac OS, Linux, Windows) so as to enable student practice at home, (ii) easy to deploy, (iii) easy to use and to take charge of, and (iv) flexible enough to enable the integration of new notations and associated services. CosyVerif is a software environment dedicated to graphical notations, that provides the mechanisms and means for an easy integration of additional existing software for teaching (or demonstration) purposes. This makes it an interesting platform to establish new courses. This paper presents our experience using CosyVerif for teaching Petri nets and parametric timed automata in two universities of the Paris region, i.e. Université Pierre et Marie Curie, and Université Paris 13. We also use CosyVerif to build demonstrators of Ph.D. students' work.
LOVE 27/02/2019 Cost Linear Temporal Logic for Verification, par Maximilien Colange
Maximilien Colange, CUI Université de Genève  
Salle B107, bâtiment B, Université de Villetaneuse
27/02/2019    15:22 - 16:30
Résumé :
Qualitative formal verification aims at checking that a given formal property holds on a model, given as an automaton. The autom