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

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.”

ASCII���Screenshot

20.6.2024
Paul-André Melliès a été invité à intervenir en séance plénière au Logic Colloquium 2024 qui se tiendra du 24 au 28 Juin à l’Université de Göteborg en Suède. Il y parlera de son travail sur les automates d’ordre supérieur et le lambda-calcul profini développé à l’IRIF en collaboration avec Sam van Gool et Vincent Moreau.

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 !

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 !

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).

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 !


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

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, Bâtiment 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) On higher multiplicity hyperplane and polynomial covers for symmetry-preserving subsets of the hypercube

Suppose we want to cover all the vertices of the n-dimensional Boolean cube using a minimum number of hyperplanes. Observe that this can be done using only two hyperplanes. Moreover, no single hyperplane can cover all the vertices. Now, what if we want to cover only a subset of the Boolean cube? For example, suppose we want to cover all the vertices except one, viz. the origin. One can observe that n hyperplanes are sufficient. But can we do better? The celebrated covering result by Alon and Füredi shows that at least n hyperplanes will be required to cover all the vertices of the n-dimensional cube leaving out exactly one vertex.

We shall discuss different versions of this covering problem, and give a generalization of Alon and Füredi’s covering result for any symmetric subset of the Boolean cube. Also, we shall show a strict separation between the size of a polynomial cover and a hyperplane cover.

This work was jointly done with Arijit Ghosh, Soumi Nandi, and S. Venkitesh.

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)

Preuves, programmes et systèmes
Jeudi 27 juin 2024, 10 heures 30, ENS Lyon
Tba Séminaire CHOCOLA

Séminaire des membres non-permanents
Jeudi 27 juin 2024, 16 heures, Salle 3052
Roman Kniazev Non encore annoncé.

Automates
Vendredi 28 juin 2024, 14 heures, Salle 3052
Lucas Larroque Non encore annoncé.

Graph Transformation Theory and Applications
Vendredi 28 juin 2024, 15 heures, online
Adrian Rutle And Uwe Wolter (Western Norway University; University of Bergen) Multilevel Typed Graph Transformations

Multilevel modeling extends traditional modeling techniques with a potentially unlimited number of abstraction levels. Multilevel models can be formally represented by multilevel typed graphs whose manipulation and transformation are carried out by multilevel typed graph transformation rules. These rules are cospans of three graphs and two inclusion graph homomorphisms where the three graphs are multilevel typed over a common typing chain. In this paper, we show that typed graph transformations can be appropriately generalized to multilevel typed graph transformations improving preciseness, flexibility and reusability of transformation rules. We identify type compatibility conditions, for rules and their matches, formulated as equations and inequations, respectively, between composed partial typing morphisms. These conditions are crucial presuppositions for the application of a rule for a match—based on a pushout and a final pullback complement construction for the underlying graphs in the category —to always provide a well-defined canonical result in the multilevel typed setting. Moreover, to formalize and analyze multilevel typing as well as to prove the necessary results, in a systematic way, we introduce the category of typing chains and typing chain morphisms.

Zoom meeting registration link

YouTube live stream