L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris-Diderot, qui héberge deux équipes-projets INRIA.

Les objectifs scientifiques de l'IRIF se situent au cœur de l'informatique, et plus particulièrement sur la conception, l'analyse, la preuve et la vérification d'algorithmes, de programmes et de langages de programmation. Ils s'appuient sur des recherches fondamentales développées à l'IRIF en combinatoire, graphes, logique, automates, types, sémantique et algèbre.

L'IRIF regroupe près de deux cents personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), et trois sont membres de l'Institut Universitaire de France (IUF).


LICS

21.05.2018
Pierre Vial (IRIF) will present at LICS 2018 an excerpt of his PhD work at IRIF proving that every lambda-term has an infinite linear representation in the infinitary relational model. This work pioneers a technique that allows giving a semantic even to unproductive programs.

LICS

13.05.2018
Paul-André Melliès (IRIF) will present at LICS 2018 his work on ribbon tensorial logic, a primary logic designed to reveal the secret topology of reasoning. This is the first time that logical proofs are faithfully translated into topological tangles using functorial knot theory.

BDA

11.05.2018
Amos Korman (IRIF) Amos Korman is co-chairing, and organizing the 6th Workshop on Biological Distributed Algorithms, to be held in London in July, the 23rd.

Institut de France

04.05.2018
Miklos Santha (IRIF) participates to the conference-debate « Calcul, communication, simulation et métrologie quantiques : des principes aux réalisations concrètes » to be held the 15 May in the Institut de France (23, quai de Conti, 75006 Paris).

IUF

27.04.2018
IRIF is proud to announce that Delia Kesner, professor of University Paris Diderot and researcher at IRIF, was appointed senior member of IUF.

LICS

23.04.2018
Six papers coauthored by IRIF members will be presented at the prestigious conference LICS'18 in Oxford this summer. Topics range from λ-calculus, to Separation Logic…

Google

06.04.2018
Victor Lanvin (PhD student of Giuseppe Castagna, IRIF) is awarded the Google PhD fellowship! Through the FSMP, Google will give a significant support to Victor's research work.

Numeration 2018

03.04.2018
The conference Numeration 2018 will be held on May 22-25 at the Univerity Paris Diderot, and is organized by Valérie Berthé, Christiane Frougny and Wolfgang Steiner from IRIF.

Kappa

28.03.2018
“The Kappa platform for rule-based modeling”, a collaboration between Jean Krivine (IRIF) and researchers from Harvard University, ENS and Santa Cruz University will be presented at ISMB2018.

STOC

02.03.2018
Adrian Kosowski (IRIF), together with Bartek Dudek (University of Wroclaw), will present at STOC 2018 a new protocol for spreading information in a population. This is the first time that methods of oscillatory dynamics are used to solve a basic task of information dissemination.

IRIF

27.02.2018
Constantin Enea (IRIF) is an organizer of the 2018 edition of the EPIT research school, on the subject of software verification, to he held in Aussois on May 7-11 2018.

IRIF

27.02.2018
Peter Habermehl (IRIF) and Benedikt Bollig (LSV, ENS Paris-Saclay) organize the research school MOVEP (Modelling and Verification of Parallel Processes), from on July 16-20 in Cachan.

Séminaire des doctorants
mercredi 23 mai 2018, 11h00, Salle 3052
Léo Stefanesco (Algebra and calculus, proofs and programs teams) An Asynchronous Soundness Theorem for Concurrent Separation Logic

The talk will start with an introduction to (concurrent) separation logic.

Abstract:

Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this talk, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems [C]S and [C]L which describe the operational behavior of the Code when confronted to its Environment, both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ ⊢ {P}C{Q} defines a winning and asynchronous strategy [π] with respect to both asynchronous semantics [C]S and [C]L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map L : [C]S → [C]L from the stateful semantics [C]S to the stateless semantics [C]L satisfies a basic fibrational property. We advocate that this fibrational property provide a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.

(Joint work with Paul-André Melliès)

Combinatoire énumérative et analytique
jeudi 24 mai 2018, 12h10, Salle 1007
Pablo Rotondo (IRIF et GREYC) Continued Logarithm Algorithm: A probabilistic study

Introduced by Gosper in 1978, the Continued Logarithm Algorithm computes the gcd of two integers efficiently, performing only shifts and subtractions. Shallit has studied its worst-case complexity in 2016, showing it to be linear. Here, we perform the average-case analysis of the algorithm: we study its main parameters (number of iterations, total number of shifts) and obtain precise asymptotics for their mean values, with explicit constants. Our analysis involves the dynamical system underlying the algorithm, which produces continued fraction expansions whose quotients are powers of 2. Even though studied by Chan in 2005, this system from an Ergodic Theory perspective, the presence of powers of 2 in the quotients gives a dyadic flavour which cannot be analysed only with Chan's results. Thus we introduce a dyadic component and deal with a two-component dynamical system. With this new mixed system at hand, we provide a complete average-case analysis of the algorithm.

Catégories supérieures, polygraphes et homotopie
vendredi 25 mai 2018, 14h00, Salle 1007
Martin Szyld (Université de Buenos Aires) The homotopy relation in a category with weak equivalences

I will present the results of the article (arXiv:1804.04244) which deals with the classical construction of the homotopy category of a model category (which is done by performing a quotient of the arrows by the homotopy relation) in the context of categories with weak equivalences. By studying this situation in an abstract context, one can define a relation of homotopy “only with respect to the weak equivalences” which yields the desired localization and coincides with the classical one for model categories. As it is usually the case, the proofs of these results, which consider only a family of arrows instead of three, become simpler. In particular, they allowed a generalization to bicategories in a current work with E. Descotte and E. Dubuc, which I will present too if time permits.

Automates
vendredi 25 mai 2018, 14h30, Salle 3052
Ulrich Ultes-Nitsche (University of Fribourg) A Simple and Optimal Complementation Algorithm for Büchi-Automata

In my presentation, I am going to present joint work with Joel Allred on the complementation of Büchi automata. When constructing the complement automaton, a worst-case state-space growth of O((0.76n)^n) cannot be avoided. Experiments suggest that complementation algorithms perform better on average when they are structurally simple. We develop a simple algorithm for complementing Büchi automata, operating directly on subsets of states, structured into state-set tuples, and producing a deterministic automaton. Then a complementation procedure is applied that resembles the straightforward complementation algorithm for deterministic Büchi automata, the latter algorithm actually being a special case of our construction. Finally, we prove our construction to be optimal, i.e. having an upper bound in O((0.76n)^n), and furthermore calculate the 0.76 factor in a novel exact way.

Vérification
lundi 28 mai 2018, 11h00, Salle 1007
Ana Sokolova (Universität Salzburg, Austria) Linearizability of Concurrent Data Structures via Order Extension Theorems

The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Verifying linearizability is a difficult, in general undecidable, problem.

In this talk, I will discuss the semantics of concurrent data structures and present recent order extension results (joint work with Harald Woracek) that lead to characterizations of linearizability in terms of violations, a.k.a. aspects. The approach works for pools, queues, and priority queues; finding other applications is ongoing work. In the case of pools and queues we obtain already known characterizations, but the proof method is new, elegant, and simple, and we expect that it will lead to deeper understanding of linearizability.

Algorithmes et complexité
mardi 29 mai 2018, 11h00, Salle 1007
Steve Alpern (University of Wariwick, UK) Shortest Paths in Networks with Unreliable Directions

The work of Korman and others, based on investigations of navigational techniques of ‘crazy ants’, leads to the following problem: Let Q be a network with given arc lengths, and let H be a ‘home’ node. At each node a permanent direction is given (one of the adjacent arcs) which leads to a shortest path path from that node to H with probability p less than one. Starting from a node S, a searcher chooses the given direction at each reached node with probability q; otherwise he chooses randomly. He arrives home at node H in expected time T=T(S,H,p,q). How should q be chosen to minimize T? Perhaps when reaching a node the searcher sees its degree k so chooses the given direction with probability q(k). Related problems have been studied for tree from a graph theoretical perspective.