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

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 !

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 !

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 !

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
Mardi 25 juin 2024, 9 heures 15, Amphi Turing @ Sophie Germain
Pps Members, All Hands On Deck ! (PPS) Journée PPS

https://www.irif.fr/rencontres/pps2024/index

To be debated: same philosophical questions as the preceding 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

Automates
Vendredi 28 juin 2024, 14 heures, Salle 3052
Lucas Larroque Normalisations of Existential Rules: Not so Innocuous!

Querying data sometimes calls for a logical layer between the user and the data to solve issues that arise with distributed datasets, overspecific vocabulary or incompleteness. Existential rules are an expressive knowledge representation language used for this purpose. In the literature, they are often supposed to be in some normal form that simplifies technical developments. Such assumptions are considered to be made without loss of generality as long as all sets of rules can be normalised while preserving entailment. However, an important question is whether the properties that ensure the decidability of reasoning are preserved as well. In this talk, I will start with presenting the chase algorithm, which is used to query data in the presence of existential rules. I will then discuss the impact of a normalisation procedure called atomic decomposition over termination of the chase. This discussion will lead me to present other results related to chase termination of (not so) independent interest.

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

Formath
Lundi 1 juillet 2024, 14 heures, 3071 and bbb Link
Victor Blanchi Non encore annoncé.

Automates
Mercredi 10 juillet 2024, 14 heures, Salle 3052
Martin Zimmermann Non encore annoncé.

Algorithmes et complexité
Vendredi 12 juillet 2024, 14 heures, Salle 3052
Nicholas Spooner (University of Warwick) An efficient quantum parallel repetition theorem and applications