## Welcome

IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and Université de Paris, 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), five 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

*9.6.2021*

Claudia Faggian (IRIF) and Francesco Gavazzo (U. Bologna) will present at LICS21 a **foundation for monadic rewriting**, and its application to calculi with algebric effects.

*9.6.2021*

Paul-André Melliès (IRIF) will present at LICS 2021 an **asynchronous template game semantics** where the shuffle tensor product of asynchronous games is formulated for the first time as the Gray tensor product of 2-categories, with appropriate scheduling template.

*8.6.2021*

Invité sur la **chaire annuelle Informatique et sciences numériques** du Collège de France 2020-2021, le Professeur Frédéric Magniez discute de la naissance de l'écosystème de l'informatique quantique. Lisez son interview !

*2.6.2021*

Thomas Ehrhard (IRIF) and Farzad Jafarrahmani (Université de Paris) will present at LICS2021 the **first categorical semantics of Linear Logic** with induction and coinduction.

*2.6.2021*

Antoine Allioux (IRIF), Eric Finster (Cambridge University), and Matthieu Sozeau (Inria) will present at LICS 2021 a proof that types are **infinity-groupoids** internal to an extension of **homotopy type theory** allowing for the formalization of higher algebraic structures.

*19.5.2021*

**Two papers** coauthored by IRIF members will be presented at the Latin and American Algorithms, Graphs and Optimization Symposium (LAGOS), **May 17-21**.

*26.5.2021*

IRIF has the great pleasure to welcome a **new research scientist (CNRS)** : Pierre-Evariste Dagand, an expert in language programming. Learn more about him and his work.

*21.5.2021*

Hugo Moeneclaey (IRIF) will present at LICS 2021 a construction semi-cubical models of type theory as cofree parametric models.

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

## Events

Verification

Monday June 14, 2021, 11AM, 3052 and BBB link

**Arnaud Sangnier** (IRIF, Université de Paris) *Reachability in Distributed Memory Automata*

This is a joint work with Benedikt Bollig and Fedor Ryabinin.

Algorithms and discrete structures

Tuesday June 15, 2021, 2PM, Salle 3052

**Magnús Halldórsson** (Reykjavik University) *New Vistas in Distributed Graph Coloring*

We present a new approach for randomized distributed Delta+1-coloring that is dramatically simpler than the previous best: the seminal work of Chang, Li, and Pettie (CLP) in SICOMP 2020. This approach offers numerous refinements: It matches the O(log^3 log n) round complexity in general, while on high-degree graphs (Delta » log^2 n), it uses only O(log* n) rounds. It uses small messages, i.e., works also in the CONGEST model. It also offers tradeoffs between the number of colors used, the round complexity, and the clique number of the graph.

We expect that the approach presented will lead the way towards improved results for various coloring problems in the near future.

This is based on a paper at STOC'21, joint work with Fabian Kuhn, Yannic Maus, and Tigran Tonoyan; and a more recent one on arXiv, joint with Alexandre Nolin, and Tigran Tonoyan.

One world numeration seminar

Tuesday June 15, 2021, 2:30PM, Online

**Sam Chow** (University of Warwick) *Dyadic approximation in the Cantor set*

Type theory and realisability

Wednesday June 16, 2021, 2PM, online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7)

**Félix Castro** (IRIF) *Proving Church Thesis in Heyting Arithmetic with Lisp's quote*

Proofs, programs and systems

Thursday June 17, 2021, 10AM, Online

**Sonia Marin** *Focused nested calculi applied to the logic of bunched implications*

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.

Automata

Friday June 18, 2021, 2:30PM, https://bbb-front.math.univ-paris-diderot.fr/recherche/ama-bgy-hx5-3rl

**Charles Paperman** *To be announced.*