Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, et héberge une équipe-projet Inria.

Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques.

L'IRIF regroupe près de deux cents personnes. Sept de ses membres ont été lauréats de l'European Research Council (ERC), trois sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences.

Suivez nous sur Mastodon, Twitter/X et LinkedIn :

LinkedIn Twitter/X Mastodon

6.6.2024
Le prix Alonzo Church 2024 (EACSL) a été attribué à Thomas Ehrhard (Directeur de recherche à l'IRIF - CNRS) et Laurent Regnier. Ce prix récompense une contribution exceptionnelle à la logique et à l'informatique. Toutes nos félicitations à tous les deux !

12.6.2024
Elixir a lancé sa nouvelle version ! Giuseppe Castagna (directeur de recherche à l'IRIF) et Guillaume Duboc (Doctorant à l'IRIF) ont développé avec José Valim le système de types pour ce langage de programmation open-source. “Cette version introduit des types ensemblistes pour un certain nombre de constructions du langage.”

30.5.2024
Un poste d'Ingénieur de recherche en développement logiciel est à pourvoir. N'hésitez pas à partager cette offre de poste autour de vous !

30.5.2024
Un poste de gestionnaire administratif-ve et financier-ère est à pourvoir ! Vous souhaitez intégrer une équipe sympathique et vous aimez le chocolat ? Ce poste est fait pour vous !

30.5.2024
La 14ème journée francilienne de programmation se déroulera le lundi 10 juin 2024 à l'Université Paris Cité, UFR d'informatique. Cette journée est l'occasion d'une confrontation ludique et amicale entre équipes d'étudiants de licence d'informatique venues de l'université Paris Saclay, de l'université Paris Cité et de Sorbonne Université. Cette journée est organisée conjointement par Pierre Letouzey (IRIF), Jean-Baptiste Yunès (UPC), Emmanuel Chailloux (UPMC) et Jean-Christophe Filliâtre (Paris Saclay).

perso-ahmed-bouajjani.jpg

27.5.2024
Ahmed Bouajjani, Professeur à l'IRIF, a été récompensé pour sa contribution à la recherche dans le domaine de l'informatique. Il a été nominé dans la catégorie Recherche scientifique pour la 6ème édition des Trophées Marocains du Monde. Toutes nos félicitations !


(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Preuves, programmes et systèmes
Jeudi 20 juin 2024, 11 heures, Salle 3052 & online (Zoom link)
Jan Vitek (Northeastern University) Reusing Just-in-Time Compiled Code

Most code is executed more than once. If not entire programs then libraries remain unchanged from one run to the next. Just-in-time compilers expend considerable effort gathering insights about code they compiled many times, and often end up generating the same binary over and over again. We explore how to reuse compiled code across runs of different programs to reduce warm-up costs of dynamic languages. We propose to use speculative contextual dispatch to select versions of functions from an off-line curated code repository. That repository is a persistent database of previously compiled functions indexed by the context under which they were compiled. The repository is curated to remove redundant code and to optimize dispatch. We assess practicality by extending Ř, a compiler for the R language, and evaluating its performance. Our results suggest that the approach improves warmup times while preserving peak performance.

Séminaire des membres non-permanents
Jeudi 20 juin 2024, 16 heures, Salle 1020
Jean Abou Samra Parsing: from theory to practice and back

As Russ Cox put it, “Historically, regular expressions are one of computer science's shining examples of how using good theory leads to good programs. Today, regular expressions have also become a shining example of how ignoring good theory leads to bad programs.” In this talk, I will first review the classical theory of parsing: context-free grammars, pushdown automata, regular expressions, efficient algorithms such as LL(k), LR(k), LALR and Thompson. Next, I will describe several extensions of these tools devised by practitioners, among which PEG grammars, and extended regular expressions. The complexity consequences of these extensions have led to entire classes of software vulnerabilities such as regular expression denial of service (ReDOS), which exploits extended regular expressions of high matching complexity. I will explain how this gives rise to interesting theoretical questions, such as “Can we decide if an extended regular expression is vulnerable?”, and conclude with a state of the art of current research on this topic. There are no prerequisites.

La syntaxe rencontre la sémantique
Jeudi 20 juin 2024, 14 heures, Salle 3052
Victor Arrial (IRIF, Universite Paris Cite) The Benefits of Diligence

In this talk, we will discuss the strength of embedding Call-by-Name (dCBN) and Call-by-Value (dCBV) into a unifying framework called the Bang Calculus (dBANG). These embeddings enable establishing (static and dynamic) properties of dCBN and dCBV through their respective counterparts in dBANG. While some specific static properties have been already successfully studied in the literature, the dynamic ones are more challenging and have been left unexplored. We accomplish that by using a standard embedding for the (easy) dCBN case, while a novel one must be introduced for the (difficult) dCBV case. Moreover, a key point of our approach is the identification of dBANG diligent reduction sequences, which eases the preservation of dynamic properties from dBANG to dCBN/dCBV. We illustrate our methodology through two concrete applications: confluence/factorization for both dCBN and dCBV are respectively derived from confluence/factorization for dBANG.

Automates
Vendredi 21 juin 2024, 14 heures, 3052
Marc Zeitoun Nested temporal hierarchies of regular languages

In this talk, we focus on unary temporal logic over words (UTL). It is known that languages definable in this logic have several equivalent characterizations based on different formalisms. Additionally, it is known that one can decide whether a regular language can be expressed in UTL.

First, I will present these various characterizations. Then, I will introduce a general approach that encompasses all known results and allows us to obtain new ones. This approach relies on the use of an “operator” whose repeated application yields a hierarchy of classes of regular languages. Finally, I will present some results about this new hierarchy, in particular its relationship with the so-called concatenation hierarchy. This is joint work with Thomas Place.

Soutenances de thèses
Vendredi 21 juin 2024, 9 heures 30, 3052 (Batiment Sophie Germain)
Mickaël Laurent (IRIF, LMF) Polymorphic type inference for dynamic languages: reconstructing types for systems combining parametric, ad-hoc, and subtyping polymorphism

Programming languages can be broadly categorized into two groups: static languages, such as C, Rust, and OCaml, and dynamic languages, such as Python, JavaScript, and Elixir. While static languages generally offer better performance and more security thanks to a phase of static typing that precedes compilation (“well-typed programs cannot go wrong”), this often comes at the expense of flexibility, making programs safer but prototyping more tedious. In this defense, I present a formal system for statically typing dynamic languages, offering a compromise between safety and flexibility.

Statically typing dynamic languages poses new challenges. In particular, functions in dynamic languages can be overloaded: they can express multiple behaviors that cannot be resolved statically, but are instead selected at runtime (either by explicit type-cases or by built-in dynamic dispatch). In addition, programs typically have no (or few) type annotations. To address these problems, I present a type system that combines, in a controlled way, first-order polymorphism with intersection types, union types and subtyping, and provide an algorithm to automatically reconstruct (infer) the type of functions. This results in a type discipline in which unannotated functions are given polymorphic types (thanks to Hindley-Milner) that can capture the overloaded behavior of the functions they type (thanks to intersection types) and that are deduced by applying advanced techniques of type narrowing (thanks to union types). This makes the system a prime candidate for typing dynamic languages.

Preuves, programmes et systèmes
Lundi 24 juin 2024, 10 heures, Amphi Turing @ Sophie Germain
Pps Members, All Hands On Deck ! (PPS) Journée PPS

We will address two typical philosophical questions: What are we doing ? Where are we going ?

Algorithmes et complexité
Lundi 24 juin 2024, 14 heures, Salle 3052
Chandrima Kayal (ISI Kolkata) Non encore annoncé.

Vérification
Lundi 24 juin 2024, 11 heures, 3052 and Zoom link
Yann Thierry (LIP6) Non encore annoncé.

Preuves, programmes et systèmes
Mardi 25 juin 2024, 10 heures, Amphi Turing @ Sophie Germain
Pps Members, All Hands On Deck ! (PPS) Journée PPS

To be debated: same philosophical questions as the preceeding day.

Algorithmes et complexité
Mardi 25 juin 2024, 14 heures, Salle 3052
Atsuya Hasegawa (The University of Tokyo) On the Power of Quantum Distributed Proofs

Quantum nondeterministic distributed computing was recently introduced as dQMA (distributed quantum Merlin-Arthur) protocols by Fraigniaud, Le Gall, Nishimura and Paz (ITCS 2021). In dQMA protocols, with the help of quantum proofs and local communication, nodes on a network verify a global property of the network. Fraigniaud et al. showed that, when the network size is small, there exists an exponential separation in proof size between distributed classical and quantum verification protocols, for the equality problem, where the verifiers check if all the data owned by a subset of them are identical. In this paper, we further investigate and characterize the power of the dQMA protocols for various decision problems.

First, we give a more efficient dQMA protocol for the equality problem with a simpler analysis. We also show a quantum advantage for the equality problem on path networks still persists even when the network size is large, by considering “relay points” between extreme nodes. Second, we show that even in a general network, there exist efficient dQMA protocols for the ranking verification problem, the Hamming distance problem, and more problems that derive from efficient quantum one-way communication protocols. Third, in a line network, we construct an efficient dQMA protocol for a problem that has an efficient two-party QMA communication protocol. Finally, we obtain the first lower bounds on the proof and communication cost of dQMA protocols.

Based on joint work with Srijita Kundu and Harumichi Nishimura (https://arxiv.org/abs/2403.14108)