## 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 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), three are members of the Institut Universitaire de France (IUF), and two are members of the Academia Europæa.

## Notion of the day

## News

(randomized-priority ranking)

*5.3.2019*

The Collège de France and IRIF are delighted to host as part of our IRIF Distinguished Talks Series **Robert Tarjan** (Princeton) on **March 18, 17:00** for a talk entitled “Concurrent Connected Components”

*15.3.2019*

**From March 20th to May 22nd, Uri Zwick** (Univ. of Tel Aviv) will give a series
of **7 courses** related to his FSMP Chaire of Excellence on the topic
of Games on Graphs and Linear Programming Abstractions each
**Wednesday 2:15pm - 4:15pm at IRIF, room 3052**.

*14.3.2019*

FSMP offers **21 PhD student positions** in Maths and TCS under H2020 COFUND project MathInParis. As a member of the FSMP network, IRIF is an eligible hosting lab.
Call for application is open until **April, 1st 2019**. Applicants must be international students, but master students already in France for less than a year are eligible.

*5.11.2018*

Amélie Gheerbrand and Cristina Sirangelo from IRIF co-organize with L. Libkin, L. Segoufin, and P. Senellart, the *2019 Spring School on Theoretical Computer Science* (**EPIT**) on *Databases, Logic and Automata*, to happen the **7-12 April 2019** in Marseille. Preregistration before **13 January 2019**.

*8.1.2019*

IRIF has the great pleasure to welcome a new researcher (CNRS), Amaury Pouly, an expert in continuous models of computations, and the analysis and verification of continuous/hybrid dynamical systems.

*17.3.2019*

The Paris Region PhD2 program will grant **30 PhD projects** on Digital Sciences and with an industrial partner. IRIF is an eligible
hosting lab.
Call for application is open until **May, 15th 2019**.

*17.1.2019*

Pierre Fraigniaud from IRIF organizes the Workshop Complexity and Algorithms (CoA), in the framework of GdR IM, Roscoff, France, **April 1-5, 2019**. The objective of this workshop is to gather the French community on design and analysis of algorithms, of all forms.
**Deadlines**: submission by 01/02/2019, registration by 02/03/2019.

## Events

IRIF seminar

Monday March 18, 2019, 5PM, Amphithéâtre Guillaume Budé - Marcelin Berthelot - Collège de France

**Robert Tarjan** (Princeton University and Intertrust Technologies) **IRIF Distinguished Talks Series**: Concurrent Connected Components

This talk is organized in collaboration with the Collège de France.

Verification

Monday March 18, 2019, 11AM, Salle 1007

**Glen Mével** (INRIA Paris) *Time Credits and Time Receipts in Iris*

Semantics

Monday March 18, 2019, 2PM, Salle 3052

**Michel Schellekens** (University College Cork) *Expedient Algebra: Duality and Entropy Conservation*

We show that EXP-computations, made reversible through history-keeping, act as closed systems in which entropy is conserved. Thus modularity of timing is linked to entropy conservation of data flow, sharpening traditional entropy preservation guaranteed by the second law of thermodynamics for reversible systems. This type of conservation typically holds for the case of energy, but not for entropy. A salient point is that for algorithms satisfying distribution control, entropy is neither created nor destroyed, merely transferred from one form, i.e. quantitative entropy, to another, i.e. positional entropy.

We establish the Entropy Conservation Laws ECL-1 and ECL-2. ECL-1 expresses the inverse proportionality of positional and quantitative entropy for distributions over series-parallel orders and their duals. ECL-2, a computational version of entropy conservation, expresses that order established by the expedient product (with history) on labels is proportionally destroyed on indices by a shadow transformation in the dual space. The laws shed new light on the properties of algorithms for which distribution control, and hence modular timing, is guaranteed.

Logic, automata, algebra and games

Wednesday March 20, 2019, 2:15PM, 3052

**Uri Zwick** (Blavatnik School of Computer Science) *Games on Graphs and Linear Programming Abstractions, Part 1/7: Two-player Turn-based Stochastic Games*

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Special talks

Wednesday March 20, 2019, 1PM, Salle 3052

**Lin Chen** (LRI) *Algorithm Design and Analysis in Wireless Networks*

Proofs, programs and systems

Thursday March 21, 2019, 10:30AM, Salle 3052

**Paolo Pistone** (Univ. Tubingen) *Quelques résultats sur l'équivalence des preuves dans la logique linéaire du second ordre*

Font partie de ces sémantiques “effaçantes” les sémantiques cohérente et rélationnelle, ainsi que la sémantique dinaturelle et la sémantique observationnelle. On présente des résultats sur l'équivalence des preuves dans ces sémantiques et on discute des applications en complexité dues à la possibilité de compresser les preuves. Une partie de ces travaux est issue d'une collaboration avec L. Tortora de Falco, T. Seiller et L.T.D. Nguyễn.

Special talks

Thursday March 21, 2019, 1PM, Salle 3052

**Reem Yassawi** (Université de Lyon) *Les automates cellulaires et dynamique symbolique*

Le premier problème concerne les propriétés de randomisation de certains automates cellulaires. La randomisation asymptotique est le processus par lequel un état initial de basse entropie est asymptotiquement transformée en un état d'entropie maximale, par l’action itérée de l’automate cellulaire. Je discute des conditions nécessaires et suffisantes pour qu’une telle randomisation survienne, et aussi d'un travail récent avec Eric Rowland.

La deuxième problématique est de caractériser les automates cellulaires qui préservent un langage donné. Je résume un travail récent avec Clemens Muellner, où nous obtenons un théorème de structure pour les automates cellulaires qui préservent certains langages HD0L.

IRIF Cake

Thursday March 21, 2019, 5:30PM, in front of room 3052

**Simon Maurras** (IRIF Cake^{TM}) *Gâteau de l'IRIF*

^{TM}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.

Automata

Friday March 22, 2019, 2:30PM, Salle 3052

**Reem Yassavi** (CNRS, Institut Camille Jordan - Université Lyon 1 - Claude Bernard) *Versions quantitatives du théorème de Christol*

Andrew Bridy a récemment donne une démonstration du théorème de Christol en utilisant des outils qui proviennent de la géométrie algébrique. Avec cette démonstration il majore le nombre d’états par une borne qui est optimale. Nous obtenons des bornes presque semblables par une démonstration élémentaire, et nous traçons les liens entre notre démonstration et celle de Bridy. Ceci est un travail en commun avec Boris Adamczewski.

Verification

Friday March 22, 2019, 11AM, 3052

**Matteo Maffei** (TU Wien) *Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts*

This talk will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust, a framework for the static analysis of Ethereum smart contracts that we recently designed, which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first steps towards a static analysis for EVM bytecode, based on Horn clause resolution, that comes with a proof of soundness.

Graphs

Friday March 22, 2019, 2PM, Salle 1007

**Julien Baste** (Universität Ulm, Ulm, Germany) *Hitting minors on bounded treewidth graphs*

The presented results are joint work with Ignasi Sau and Dimitrios Thilikos and can be found in <https://arxiv.org/abs/1704.07284>.

Verification

Monday March 25, 2019, 11AM, Salle 1007

**Cristoph Kirsch** (Universität Salzburg) *On the Self in Selfie*

This is joint work with Alireza S. Abyaneh, Simon Bauer, Philipp Mayer, Christian Mösl, Clément Poncelet, Sara Seidl, Ana Sokolova, and Manuel Widmoser, University of Salzburg, Austria.