## 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. Seven 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

## Social Networks

Follow us on Twitter/X, LinkedIn and Mastodon for our latest news:

## News

*5.11.2024*

This year, three IRIF researchers are part of two projects that have won a **2025 Synergy Grant from the European Research Council (ERC)**. Many congratulations to Valérie Berthé, Hugo Herbelin and Paul-André Melliès ! IRIF wishes them successful results.

*12.11.2024*

The **LVP (Languages and Program Verification) working group** of the GPL GdR of the CNRS will be holding its one-day conference on **Thursday 14 November** 2024 at **IRIF, from 9am to 5.40pm**. Emilio Jesús Gallego Aria, Inria researcher at IRIF, University of Paris, will be giving a talk on : ‘Flèche: Incremental Validation for Hybrid Formal Documents’. This event is free but registration is required.

*24.10.2024*

The **Innovation Prize** has been awarded to Sergio Rajsbaum, associate member of IRIF, in recognition of his **significant contribution to Distributed Computing**. The prize will be presented to him at the **SIROCCO'25** conference in Delphi, Greece.

*24.10.2024*

* Does Computer Science Have a Future?* That is the question to be debated during the third conference, “We Turn Off, We Reflect, We Discuss,” organized at Université Paris Cité by François Laroussinie. José Halloy (LIED) and Anne-Laure Ligozat (LISN) are the invited speakers. It will take place on

**December 10, 2024**, from

**4:15 PM to 6:30 PM**. This event is free of charge.

*31.10.2024*

IRIF is excited to host Dexter Kozen from Cornell University as a speaker in our Distinguished Talks series. The talk will take place on **December 03, 2024, starting at 11a.m**. More details to come!

*30.9.2024*

Jean-Louis Krivine, Professor Emeritus at IRIF, has published a book entitled ‘Les décompilateurs - L'Univers en tête’. In it you will find, among other things, a reflection on the **origin of mathematics** and the **link between logic and theoretical computing**, as well as some **paradoxes in quantum mechanics**.

*25.9.2024*

CNRS Computer Science is organizing the conference “**Optimization: at the Heart of Challenges in Computer Science**” which will take place on **October 3, 2024**, at the CNRS Headquarters. This event, aimed at industry professionals, decision-makers, and journalists, brings together the scientific community to exchange and share knowledge on this cross-disciplinary topic. Claire Mathieu, Simon Apers and David Saulpic will give talks.

*18.9.2024*

Neha Rino (MPRI intern at IRIF in 2023), Eugène Asarin and Mohammed Foughali won the **Best Paper Award at FORMATS**. This work **formulate and solve** by an efficient algorithm the **problem of quantitative monitoring**: compute a real number characterizing to which extent the given trace of a real-time system satisfies its specification.

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

## Agenda

Automata

Friday November 15, 2024, 2PM, Salle 3052

**Luc Dartois** (LACL) *Reversible Transducers over Infinite Words*

PhD defences

Friday November 15, 2024, 10AM, Salle 279F, Halle aux farines

**Colin González** (IRIF) *From spreadsheets to functional programs: compilation and efficient execution of structured spreadsheets*

This thesis proposes a new perspective on spreadsheet development by adopting the principles of structured programming. Through the development of Lisa, a domain specific language, we propose the structured programming approach for spreadsheets. The main feature of this approach is to organise the sheets by columns rather than by cells. In this way, we can model the columns as potentially infinite streams of data. The unique aspect of this language is the introduction of indexed streams. In this context, the indexed nature of the streams capture the notion of the current row number of a given column’s cell. A relative access (relative to the current index) operation allows preserving a programming style akin to that of formulae found in traditional spreadsheets. The remainder of the thesis addresses the design and implementation of Lisa, a functional language focused on programming with indexed streams. In particular, we cover the compilation of Lisa into executables for various execution targets, ranging from traditional hardware platforms to the blockchain. Moreover, the programs issued by the compilation process depend on a runtime environment providing the relative access operator and indexed streams. The implementation of this operation is particularly slow for classical implementations of streams. To address these performance issues, we propose a new way of programming streams that is well suited to accelerating this key operation.

Lisa is a fundamental component for the design of a specialised spreadsheet software tailored for the development of structured spreadsheets. In such a spreadsheet software, Lisa is used both to implement the formulae of a sheet and to develop extensions in the form of macro definitions. Finally, the compiled approach allows generating, from a structured sheet, an executable compatible with various software interfaces, thus enabling the modular composition of spreadsheet application developments, carried by end users, with highly technical software components developed by specialists.

Verification

Monday November 18, 2024, 11AM, Salle 3052

**Romain Delpy** (LaBRI, Univ. Bordeaux) *An Automata-based Approach for Synchronizable Mailbox Communication*

A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. We know from previous results that reachability is PSPACE-complete for synchronizable systems.

In this talk we show that we can check if a mailbox system is synchronizable thanks to a novel automata-based approach. From this we get that checking synchronizability is PSPACE-complete. The same question is undecidable under peer-to-peer semantics. We also show that model-checking synchronizable systems for a natural subclass of regular properties is a PSPACE-complete problem.

Joint work with Anca Muscholl & Grégoire Sutre.

Programming

Monday November 18, 2024, 10AM, 3071

**Guillaume Baudart** (IRIF) *Natural Language Intermediate Representation for Mechanized Theorem Proving*

Enumerative and analytic combinatorics

Tuesday November 19, 2024, 11AM, Salle 3071

**Clément Chenevière** (LISN, Université Paris-Saclay) *Une nouvelle description des treillis m-cambriens*

Dans un travail en cours avec Wenjie Fang et Corentin Henriet, nous proposons une nouvelle définition équivalente des treillis m-cambriens. Nous donnons un critère de comparaison simple et effectif sur des objets simples appelés m-partitions non croisées. Cette définition est obtenue en montrant qu'il existe une unique chaîne c-croissante entre n'importe quelle paire d'éléments comparables, et cette dernière est calculée par un algorithme glouton. Ce faisant, nous introduisons un ordre partiel intéressant sur les intervalles d'un treillis cambriens, qui est nouveau, même pour le cas du treillis de Tamari.

Proofs, programs and systems

Tuesday November 19, 2024, 3PM, TBA

**Pedro Amorim** *To be announced.*

Algorithms and complexity

Tuesday November 19, 2024, 11AM, Salle 3052

**Philip Verduyn Lunel** (LIP6) *Quantum Position Verification Protocols: Security and Practical Considerations*

Thus, unconditionally-secure quantum position-verification protocols do not exist. From a practical point of view, not all is lost. The exponential upper bound for a general attack is still astronomically large for only a relatively small input. Thus, we can still hope for practically secure QPV protocols. This raises the problem of designing protocols that are secure in a practical setting. In this talk we will present an overview of the field and present some proposed protocols and discuss their advantages and drawbacks. We will also discuss the best known entanglement bounds.

Proofs, programs and systems

Thursday November 21, 2024, 10:30AM, ENS Lyon

**Tba** *CHOCOLA seminar series*

Non-permanent members' seminar

Thursday November 21, 2024, 4PM, Salle 3052

**Manu Catz** (PhD Student) *Polygraphs and Oriented Shapes*

References:

Polygraphs: Dimitri Ara et al. Polygraphs: From Rewriting to Higher Categories.

Orientals: Ross Street. “The algebra of oriented simplexes” ; Dimitri Ara, Yves Lafont, and François Métayer. Orientals as free algebras.

Oriented Cubes: Iain R. Aitchison. The geometry of oriented cubes.

Parametricity: Hugo Herbelin and Ramkumar Ramachandra. A parametricity-based formalization of semi-simplicial and semi- cubical sets.

Automata

Friday November 22, 2024, 2PM, Salle 3052

**Pierre Letouzey** (IRIF) *Generalizing some Hofstadter functions: G, H and beyond*

Hofstadter's G function is recursively defined via $G(0)=0$ and then $G(n)=n-G(G(n-1))$. Following Hofstadter, a family $(F_k)$ of similar functions is obtained by varying the number $k$ of nested recursive calls in this equation. We present here a few nice properties of these functions. In particular, they can be described via some infinite morphic words generalizing the Fibonacci word. This was crucial for proving that this family is ordered pointwise: for all $k$ and $n$, $F_k(n) \le F_{k+1}(n)$. Moreover, these functions have a simple behavior on well-chosen numerical representations (Zeckendorf decompositions for some Fibonacci-like sequences). Thanks to that, we were also able to estimate the discrepancies for these $F_k$, i.e. the maximal distances between each $F_k$ and its linear equivalent. This whole work was formally proved using the Coq proof assistant (except for a beautiful fractal!) and we will give a gentle introduction to this Coq development.