## Welcome

IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team.

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), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences.

## Notion of the day

## News

*31.5.2023*

Geoffroy Couteau et Pierre-Evariste Dagand ont écrit un texte à quatre mains dans le Blog Binaire du Journal Le Monde. Ils se demandent s'il est possible de **contrôler l'accès aux sites pornographiques** tout en conservant l'anonymat et les données de l'utilisateur pour protéger les enfants. C'est ici que le **“zéro-proof knowledge”** rentre en jeux…

*4.5.2023*

Le pôle PPS organise ses journées 2023, les 25 et 26 mai prochains, et c'est ouvert à tous.

*15.5.2023*

Congratulations to Jean Krivine (IRIF) and Vincent Danos (ENS and CNRS) who have received the Concur Test-of-Time Award (period 2002-2005) for their article “Reversible Communicating Systems”, published at CONCUR 2004. To read their article :

*11.5.2023*

À l’occasion du départ à la retraite de **François Métayer**, le **LHC** rendra hommage au spécialiste des polygraphes, de l’homotopie et de la réécriture, animateur d’un groupe de travail mythique sur ces sujets. L’événement aura lieu les ***8 et 9 juin 2023** et sera précédé par les journées LHC

*5.4.2023*

The ANR CoREACT will have its kick-off on Wednesday 19 April. It will be in room 146 and online, open to everyone. Contact Nicolas Behr for the details.

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

## Agenda

Verification

Monday June 5, 2023, 11AM, Olympe de Gouges 146 and Zoom link

**Pedro Ribeiro** (University of York) *Co-verification for robotics: simulation and verification by proof*

Formath

Monday June 5, 2023, 2PM, 146 (Olympe de Gouges)

**Wendlasida Ouedraogo** (INRIA (Paris Saclay)) *Source code optimization for safety critical systems*

This research work is situated in the context of one such system, the communication-based train control (CBTC) system of Siemens Mobility France which operates a number of driverless subway systems around the World, including Paris lines 1, 4, and 14. That system is certified according to the industrial norm EN-50128 and up to the highest Safety Integrity Level 4, required for safety-critical systems with potentially catastrophic consequences. In this context, the thesis looks for an answer to the question of how to automatically optimize the execution time performance of such systems without losing the previously obtained safety guarantees.

The answer provided is provably correct optimization of source code. A first contribution is a source-to-source compiler for VCP Ada (a subset of Ada) programs, that optimizes source code while preserving the formal semantics of the programs. The compiler has been proven correct in the Coq proof assistant and guarantees the equivalence of execution between the original and the optimized program. The compiler copes with the complexities of the platform, due to hardware safety measures, which is important, since real-world safety-critical systems are often susceptible to having such measures, potentially conflicting with existing formally proven optimizing compilers. Moreover, choosing the approach of a source-to-source compilation shows to have methodological advantages over an approach to proven optimizations having a number of intermediate languages, allowing to simplify and diminishing the needed proof effort.

A second contribution is to the problem of provably correct lexical analysis of compilers, which has previously not received a lot of research attention, a weak link in any compilation chain using a proven or qualified compiler. We develop CoqLex, the first Coq-formalized lexer generator, based on a modification of an existing Coq implementation of regular expression matching via Brzozowski derivatives.

The developed theory and tools have been applied to optimize real-world VCP Ada programs of CBTC systems, consisting of thousands of source files, with promising results.

Algorithms and complexity

Tuesday June 6, 2023, 11AM, Salle 147 (Olympe de Gouges)

**Galina Pass** (QuSoft, University of Amsterdam) *(No) Quantum space-time tradeoff for USTCON*

Analysis and conception of systems

Wednesday June 7, 2023, 2PM, Salle 146 (Olympe de Gouges)

**Samuel Vivien** (ENS Paris, IRIF) *How to prove that you need Cake ?*

Based on : PureCake: A Verified Compiler for a Lazy Functional Language [PLDI'23] by Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti

Enumerative and analytic combinatorics

Thursday June 8, 2023, 2PM, Olympe de Gouges

**Davig Forge** (Orsay) *TBD*

Non-permanent members' seminar

Thursday June 8, 2023, 4PM, Olympe de Gouges 147 and Zoom link

**Bernardo Jacobo-Inclan** *To be announced.*

Automata

Friday June 9, 2023, 2PM, Salle 146 Olympe de Gouges

**Daniel Smertnig** *Deciding Sequential? and Unambiguous? for weighted automata over fields*

This talk is on joint work with J. Bell.

Verification

Monday June 12, 2023, 11AM, Olympe de Gouges 146 and Zoom link

**Themistoklis Melissourgos** (University of Essex) *To be announced.*

Distributed algorithms and graphs

Tuesday June 13, 2023, 3PM, 147 Olympe de Gouges

**Anna Gujgiczer** (Budapest University of Technology and Economics, Hungary) *Circular chromatic number of generalised Mycielski graphs on odd cycles and other quadrangulations of the projective plane*

In this talk we present a new, relatively short direct proof for the circular chromatic number, using only a basic notion of algebraic topology, namely the winding number. Then we present another graph family with high odd girth and circular chromatic number 4. This construction is very similar to the generalized Mycielski, but on its first two layers it forms a M$\ddot{o}$bius ladder. We prove the statement about their circular chromatic number with similar techniques. Moreover we present a similar result for a family of signed graphs.

This talk is based on a joint work with Reza Naserasr (Universit´e de Paris, IRIF, CNRS, F-75006, Paris, France), S Rohini (Indian Institute of Technology Madras, India) and S Taruni (Indian Institute of Technology Dharwad, India).

Enumerative and analytic combinatorics

Thursday June 15, 2023, 2PM, Salle 146 - Olympe de Gouges

**Marc Noy** (UPC (Espagne)) *Chordal graphs with bounded tree-width*