IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and Université de Paris, also hosting two Inria project-teams.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

IRIF hosts about 200 people. Six of its members have been distinguished by the European Research Council (ERC), five are members of the Institut Universitaire de France IUF), and two are members of the Academia Europæa.

7.11.2019
What are near-term quantum computers good for? Iordanis Kerenidis (IRIF) will give a talk on 11/29 in a meeting organized by the DIM Sirteq where Google will present its recent results about quantum supremacy. Registration is free but mandatory.

16.10.2019
On December 16th, a half-day of talks aimed at a non-specialized audience will take place at IRIF in celebration of Algorithms, the research domain of Claire Mathieu, 2019 recipient of a CNRS Silver Medal. The event will conclude with a discussion of new research directions in Algorithms. Free Registration before November 30th.

1.11.2019
IRIF hosts the annual meeting of the molecular bioinformatics research group of CNRS (GDR BIM) from 11-05 to 11-07.

29.10.2019
Walter FONTANA (MedSchool Harvard) holds the annual chair of Collège de France on the theme “Life and the Computer: The Challenge of a Science of Organization”. The lectures and seminars started since the 10-24. Jean Krivine (IRIF) will give a seminar the 11-22.

23.10.2019
Marie Kerjean (former IRIF PhD student) is one of the recipients of the L'Oréal-Unesco award for women in science. Marie is building a bridge between logic, programming, and physics using functional analysis to model proofs, and types to understand analysis.

23.9.2019
Giuseppe Castagna (IRIF) and Jeremy Siek (Indiana) organize WGT 2020, the first ACM SIGPLAN Workshop on Gradual Typing, colocated with POPL. Submission deadline: Monday, October the 21st.

Gradual typing is a technique that allows the programmer to control which parts of a program check their type correctness (i.e., that apples are added to apples) before execution and which parts check it during their execution instead. It is often used to gradually add the before-execution check to dynamic languages, like JavaScript, which perform the check only at run-time, since it is generally better to find errors before the execution of a program rather than during its execution.

(These news are displayed using a randomized-priority ranking.)

Graphs
Tuesday November 12, 2019, 3:30PM, Salle 3052
Suchismita Mishra (IITM) Strong chromatic index of unitary Cayley graphs

A strong edge coloring of a graph is an assignment of colors to edges such that every color class induces a matching. The smallest number of colors for which a strong edge coloring of a graph G exists is known as the strong chromatic index and it is denoted by $\chi′_s(G)$. It is already known that the problem of finding the strong chromatic index for arbitrary graphs is NP-complete. In this talk, we will discuss strong edge coloring of unitary Cayley graphs.

PhD students seminar
Wednesday November 13, 2019, 11AM, Salle 3052
(New) Phd Students The PhD Seminar strikes back

Every new/old PhD student is invited to come and talk about her/his research interests.

Each talk will be 2-5 minutes long, without any slides, and should be understandable by everyone

Enumerative and analytic combinatorics
Thursday November 14, 2019, 2PM, Salle 1007
Wenjie Fang (Université Paris-Est Marne-la-Vallée) Arbres binaires compactés possède une exponentiel étiré

Un arbre binaire compacté est un graphe acyclique dirigé qui représente un arbre binaire de façon sans redondances, dans le sens que tous les sous-arbres isomorphes sont partagés. Nous montrons que le nombre des arbres binaires compactés de tailles n croît asymptotiquement en

\Theta(n! 4^n e^{3 a_1 n^{1/3}} n^{3/4}).

Ici, a_1 ≈ -2,338 est la plus grande racine de la fonction d'Airy. Ce résultat est obtenu à partir d'une nouvelle récurrence des nombres de ces arbres compactés, avec une nouvelle méthode qui, inspirée par des estimations empiriques suffissament précises, prouve des bonnes bornes par induction. Ce travail donne aussi des nouvelles bornes sur le nombre d'automates minimaux qui reconnaissent un langage fini d'un alphabet binaire, qui possède aussi un exponentiel étiré. Par sa simplicité, notre méthode s'applique potentiellement aux autres objets.

Proofs, programs and systems
Thursday November 14, 2019, 10:30AM, École normale supérieure de Lyon
Francesco Gavazzo, Marie Kerjean, Yann Régis-Gianas Séminaire Chocola

IRIF Cake
Thursday November 14, 2019, 5PM, In front of room 3052
Yassine Hamoudi, Farzad Jafar-Rhamani, Pierre Ohlmann (IRIF CakeTM) Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

Higher categories, polygraphs and homotopy
Friday November 15, 2019, 2PM, Salle 1007
Juan Pablo Vigneaux (IMJ) Une caractérisation homologique de l'entropie différentielle

Il y a plusieurs caractérisations algébriques (dites “axiomatiques”) de l'entropie discrète de Shannon. Je vais présenter ici une caractérisation analogue pour l'entropie différentielle, qui apparaît dans la théorie de compression des signaux continus: le cadre utilisé est la “cohomologie de l'information”, associé aux préfaisceaux sur certaines structures combinatoires. Si le temps le permet, je vais présenter d'autres théories cohomologiques des faisceaux très proches, définies sur les graphes (Friedman) et les complexes simpliciaux (Abramsky et al.), qui correspondent aussi à la cohomologie des topos.

Automata
Friday November 15, 2019, 2:30PM, Salle 3052
Patrick Totzke Timed Basic Parallel Processes

I will talk about two fun constructions for reachability analysis of one-clock timed automata, which lead to concise logical characterizations in existential Linear Arithmetic.

The first one describes “punctual” reachability relations: reachability in exact time t. It uses a coarse interval abstraction and counting of resets via Parikh-Automata. The other is a “sweep line” construction to compute optimal time to reach in reachability games played on one-clock TA.

Together, these can be used to derive a (tight) NP complexity upper bound for the coverability and reachability problems in an interesting subclass of Timed Petri Nets, which naturally lends itself to parametrised safety checking of concurrent, real-time systems. This contrasts with known super-Ackermannian completeness, and undecidability results for unrestricted Timed Petri nets.

This is joint work with Lorenzo Clemente and Piotr Hofman, and was presented at CONCUR'19. Full details are available at https://arxiv.org/abs/1907.01240.

Verification
Friday November 15, 2019, 2:30PM, Salle 3052
Patrick Totzke (Liverpool University) Timed Basic Parallel Processes

I will talk about two fun constructions for reachability analysis of one-clock timed automata, which lead to concise logical characterizations in existential Linear Arithmetic.

The first one describes “punctual” reachability relations: reachability in exact time t. It uses a coarse interval abstraction and counting of resets via Parikh-Automata. The other is a “sweep line” construction to compute optimal time to reach in reachability games played on one-clock TA.

Together, these can be used to derive a (tight) NP complexity upper bound for the coverability and reachability problems in an interesting subclass of Timed Petri Nets, which naturally lends itself to parametrised safety checking of concurrent, real-time systems. This contrasts with known super-Ackermannian completeness, and undecidability results for unrestricted Timed Petri nets.

This is joint work with Lorenzo Clemente and Piotr Hofman, and was presented at CONCUR'19. Full details are available at https://arxiv.org/abs/1907.01240.

Verification
Monday November 18, 2019, 11AM, Salle 1007
Arnaud Sangnier (IRIF) The Complexity of Flat Freeze LTL

We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.

PhD students seminar
Tuesday November 19, 2019, 11AM, Salle 3052
Pierre Ohlmann To be announced.

Semantics
Tuesday November 19, 2019, 10:30AM, Salle 3052
Fredrick Dahlqvist (University College London) To be announced.