## Welcome to IRIF

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

The scientific objectives of IRIF are at the core of computer science and, in particular, they focus on the conception, analysis, proof, and verification of algorithms, programs, and programming languages. They are built upon fundamental research activities developed at IRIF on combinatorics, graphs, logics, automata, type, semantics, and algebras.

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

## Notion of the day

(*refresh the page for a new one*)

## News

*15.06.2018*

Amina Doumane (former PhD student at IRIF, now at LIP) was awarded the Ackermann prize of EACSL for her PhD thesis entitled On the infinitary proof theory of logics with fixed points.

*06.06.2018*

Delia Kesner (IRIF) and Matthieu Sozeau (IRIF) will both give
invited talks entitled *“Multi Types for Higher-Order languages”*
and *“The Predicative, Polymorphic Calculus of Cumulative Inductive Constructions and its implementation”*
at TYPES 2018, held in Braga (Portugal), June 18-21.

*06.06.2018*

We are delighted to host as part of our IRIF Distinguished Talks Series
**Christos Papadimitriou** (Columbia University) on **July 13, 10:30** for a talk entitled *“A computer scientist thinks about the Brain”*.

*06.06.2018*

Today Roberto Di Cosmo (professor at IRIF) with a ceremony at UNESCO opened to the public the archives of Softwareheritage.org, a worldwide initiative to create a universal library of computer programme source codes since the dawn of the digital age. .

*01.06.2018*

Claire Mathieu (IRIF associate member) organizes a 1-day colloquium on Approximation algorithms and networks at Collège de France on ** June 7**. This is part of the Chair in Informatics and Computational Sciences at College de France in association with INRIA.

*30.05.2018*

**« Tous femmes de numérique ! »** Après leur rencontre avec **4 informaticiennes de l’IRIF**, 14 lycéennes du Lycée Jules Ferry ont expliqué à leurs camarades l’exposition permanente du Palais de la découverte sur l’informatique et les sciences du numérique le 29/05.

*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**.

*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.

## Events

Vérification

lundi 25 juin 2018, 11h00, Salle 3052

**Nicolas Jeannerod** (IRIF) *Deciding the First-Order Theory of an Algebra of Feature Trees with Updates*

The CoLiS project aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analyzing shell scripts. The data structure that is manipulated by these scripts, namely the file system tree, is a complex one.

We plan to use feature trees as an abstract representation of file system tree transformations. We thus investigate an extension of these feature trees that includes the update operation, which expresses that two trees are similar except in a particular subtree where there might have been changes.

We show that the first-order theory of this algebra is decidable via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers.

Combinatoire énumérative et analytique

mardi 26 juin 2018, 11h00, Salle 1007

**Juanjo Rué** (Universitat Politècnica de Catalunya) *Enumeration of labelled 4-regular planar graphs*

We present the first combinatorial scheme for counting labelled 4-regular planar graphs through a complete recursive decomposition. More precisely, we show that the exponential generating function of labelled 4-regular planar graphs can be computed effectively as the solution of a system of equations, from which the coefficients can be extracted. As a byproduct, we also enumerate labelled 3-connected 4-regular planar graphs, and simple 4-regular rooted maps. Finally, we discuss how to obtain asymptotic results.

This is based on joint works with Marc Noy (UPC) and Clément Réquile (TU Wien)

Séminaire des doctorants

mercredi 27 juin 2018, 11h00, Salle 3052

**Victor Lanvin** (Équipes Preuves, programmes, et Systèmes) *TBA*

Preuves, programmes et systèmes

jeudi 28 juin 2018, 10h30, Salle 3052

**Olivier Hermant** (CRI, Mines ParisTech) *Intersection Types in Deduction Modulo Theory*

In a 2012 paper, Richard Statman exhibited an inference system, based on second order monadic logic and non-terminating rewrite rules, that exactly types all strongly normalizable lambda-terms. We show that this system can be simplified to first-order minimal logic with rewrite rules, along the Deduction Modulo Theory lines.

We show that our rewrite system is terminating and that the conversion rule respects weak versions of invertibility of the arrow and of quantifiers. This requires additional care, in particular in the treatment of the latter. Then we study proof reduction, and show that every typable proof term is strongly normalizable and vice-versa.

Automates

vendredi 29 juin 2018, 14h30, Salle 3052

**Jacques Sakarovitch** (IRIF/CNRS and Telecom ParisTech) *The complexity of carry propagation for successor functions*

Given any numeration system, we call 'carry propagation' at a number N the number of digits that are changed when going from the representation of N to the one of N+1 , and 'amortized carry propagation' the limit of the mean of the carry propagations at the first N integers, when N tends to infinity, and if it exists.

We address the problem of the existence of the amortized carry propagation and of its value in non-standard numeration systems of various kinds: abstract numeration systems, rational base numeration systems, greedy numeration systems and beta-numeration.

We tackle the problem by means of techniques of three different types: combinatorial, algebraic, and ergodic.

For each kind of numeration systems that we consider, the relevant method allows to establish sufficient conditions for the existence of the carry propagation and examples show that these conditions are close to be necessary.

This is a joint work with Valérie Berthé, Christiane Frougny, and Michel Rigo

Vérification

vendredi 29 juin 2018, 11h00, Salle 3052

**Mahsa Shirmohammadi** (LIS, CNRS - Univ. Aix-Marseille) *Costs and Rewards in Priced Timed Automata*

We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.