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

affichefds2024.jpg

4.10.2024
La Fête de la Science édition 2024 est lancée ! L'IRIF et l'Université Paris Cité accueilleront du 4 au 14 octobre, 13 classes de primaire et collège, qui viendront découvrir l'informatique à travers des activités débranchées et de la programmation. Nous proposons également un programme quantique créé avec le laboratoire Matériaux et Phénomènes Quantiques (MPQ) à des classes de lycée.

optimisation_web.jpg

25.9.2024
CNRS Sciences Informatiques organise la conférence « L'optimisation : au cœur des défis de l'informatique » qui aura lieu le 3 octobre 2024, au siège du CNRS. Cet événement, destiné aux professionnels de l'industrie, aux décideurs et aux journalistes, rassemble la communauté scientifique pour échanger et partager les connaissances sur ce sujet transdisciplinaire. Claire Mathieu, Simon Apers et David Saulpic y interviendront.

jlkrivine_lesdecompilateurs.jpg

30.9.2024
Jean-Louis Krivine, professeur émérite à l'IRIF, a publié un livre, “Les décompilateurs - L'Univers en tête”. Vous y trouverez, entre autres, une réflexion sur l'origine des mathématiques et le lien entre logique et informatique théorique ainsi que quelques paradoxes en mécanique quantique.

formatsbestpaperaward2024.jpg

18.9.2024
Neha Rino (stagiaire MPRI à l'IRIF en 2023), Eugène Asarin et Mohammed Foughali ont remporté le Best Paper Award à FORMATS. Ce travail formule et résout par un algorithme efficace le problème du suivi quantitatif : calculer un nombre réel caractérisant dans quelle mesure la trace donnée d'un système temps réel satisfait sa spécification.

book_basics_of_programming_algorithms.jpeg

11.9.2024
Roberto Mantaci et Jean-Baptiste Yunès ont publié un livre intitulé « Basics of Programming and Algorithms, Principles and Applications ». Il fournit un contenu de base pour l'enseignement de la programmation et des algorithmes, couvrant l'analyse des performances des algorithmes et les connaissances essentielles en programmation Python.

Happy International Woman Day.Feminism concept.Bright Beautiful Different
Dancing Girls Holding Hands.Party,Eight of March Celebration. Free Confident...

19.9.2024
Cette année, l'IRIF s'est fixé un objectif clair : atteindre la parité parmi les stagiaires de 3e. Un véritable défi, car dans les sciences informatiques, la proportion de femmes est encore nettement plus faible. C'est pourquoi nous comptons sur nos réseaux pour attirer davantage de candidatures féminines que les années précédentes ! Une semaine dans notre laboratoire de recherche permettra aux stagiaires de découvrir l'univers de la recherche et de mieux comprendre ce qu'est l'informatique.

perso-delia-kesner.jpg

26.8.2024
Delia Kesner est oratrice invitée à la conférence internationale Lambda World qui aura lieu à Cadiz (Espagne) du 2 au 4 octobre 2024.

ashwin_nayak.jpg

2.9.2024
Ashwin Nayak (professeur à l'Université de Waterloo) sera en visite à l'IRIF de septembre à octobre 2024. Ses recherches portent sur les algorithmes quantiques, la complexité et la communication. Il a beaucoup collaboré avec le Dr Frédéric Magniez et d'autres membres de l'IRIF sur ces sujets. En s'appuyant sur leurs collaborations de recherche, le Dr. Magniez et lui-même ont dirigé un programme international d'échange d'étudiants entre le Canada et un certain nombre d'institutions de l'UE, ainsi qu'un projet PICS entre l'Institute for Quantum Computing de l'Université de Waterloo et l'IRIF. Ashwin se réjouit de renouer ces liens lors de sa prochaine visite.


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

Formath
Lundi 7 octobre 2024, 14 heures, 3052
Nadine Karsten (TU Berlin, Chair: Models and Theory of Distributed Systems) ProofBuddy - The way to teach proofs structures?

There are many ways to teach proof competence. Students try to use “perfect” proofs from textbooks or experts to create their own proofs in exercises, and they often fail. In particular, many students struggle with properly understanding the structure of proofs. We believe that—for the education of Computer Science students who are used to programming—it is natural to use proof assistants to learn to develop and write proofs. In addition, the immediate feedback from proof assistants helps students to check their proofs for correctness and completeness.

However, proof assistants are not made for beginners. Moreover, learning formal and mathematical language at the same time is often overwhelming. We develop the web interface ProofBuddy based on the proof assistant Isabelle as a tool that (also) targets for beginners. We chose Isabelle, because we assume that the proximity of its Isar language to natural/mathematical language supports the learning process. Pedagogically, we experiment with a setting in which students constantly switch between pen-and-paper-proofs and their formal counterparts. ProofBuddy is designed to support this back-and-forth approach.

In the talk, I report on the architecture and the user interface of ProofBuddy, give a short introduction to Isar within ProofBuddy and present our pedagogical approach.

Algorithmes et complexité
Mardi 8 octobre 2024, 11 heures, Salle 3052
Julia Kastner (CWI, Amsterdam) Pairing-Free Blind Signatures from Standard Assumptions in the ROM

Blind Signatures are a useful primitive for privacy preserving applications such as electronic payments, e-voting, anonymous credentials, and more.

However, existing practical blind signature schemes based on standard assumptions require either pairings or lattices. We present the first practical construction of a round-optimal blind signature in the random oracle model based on standard assumptions without resorting to pairings or lattices. In particular, our construction is secure under the strong RSA assumption and DDH (in pairing-free groups). For our construction, we provide a NIZK-friendly signature based on strong RSA, and efficiently instantiate a variant of Fischlin's generic framework (CRYPTO'06). Our Blind Signature scheme has signatures of size 4.28 KB and communication cost 10.98 KB. On the way, we develop techniques that might be of independent interest. In particular, we provide efficient *relaxed* range-proofs for large ranges with subversion zero-knowledge and compact commitments to elements of arbitrary groups.

Joint work with Michael Reichle and Ky Nguyen.

Sémantique
Mercredi 9 octobre 2024, 15 heures, Salle 3052
Joshua Wrigley (Queen Mary University of London) Capturing theories via isomorphisms: classifying topoi and topological groupoids

The Ahlbrandt-Ziegler result in model theory asserts that a countably categorical theory is characterised, up to bi-interpretability, by the topological automorphism group of its (unique) countable model, thus permitting a study of these theories by group-theoretic properties.

Removing the countable categoricity assumption necessitates using topological groupoids rather than groups. We will describe a groupoidal generalisation of the Ahlbrandt-Ziegler result using topos theory.

Our result extends the results in the topos-theoretic literature of Awodey, Butz, Caramello, Forssell and Moerdijk, while being orthogonal to the parallel generalisation of Ben Yaacov.

Combinatoire énumérative et analytique
Jeudi 10 octobre 2024, 11 heures, IHP
Séminaire Flajolet À L'Ihp semflajolet.math.cnrs.fr

Séminaire des membres non-permanents
Jeudi 10 octobre 2024, 16 heures, Salle 3052
Everyone Introductory session & social event

We will start a new series of non-permanent weekly seminars with an introduction section, during which everyone can briefly share their name, background, and research topic (if desired). This is a casual and friendly setting, so don't be shy!

After the session, we will have some refreshment and play some games, everyone is welcome.

La syntaxe rencontre la sémantique
Jeudi 10 octobre 2024, 14 heures, Salle 3052
Jorge A. Pérez (University of Groningen) The Expressiveness of Session Types

Session types are a typed approach to ensure the communication correctness of message-passing programs. They have been extensively studied from a theoretical standpoint, and have been also incorporated into diverse programming languages and models.

Perhaps surprisingly, there is no single, canonical session type system, but many. It is fair to say that expressiveness has been key to the success and impact of session types: enhancing the expressivity of typed processes and/or the properties enforced by typing is often a strong motivation for developing new typed frameworks.

In this rich and diverse context, rigorously contrasting different variants of session types from an expressiveness perspective is a fascinating and non-trivial challenge. In this talk I introduce session types briefly and overview some recent works related to their expressiveness; they cover various angles, including “propositions-as-sessions”, i.e., the Curry-Howard correspondence between session types and linear logic.

Automates
Vendredi 11 octobre 2024, 14 heures, Salle 3052
Mihir Vahanwala (MPI-SWS, Saarbrücken) On the Monadic Second-Order Theory of Arithmetic Predicates

Büchi's seminal 1962 paper established the decidability of the monadic second-order (MSO) theory of the structure (Nat; <), and in so doing brought to light the profound connections between mathematical logic and automata theory. This talk presents our recent results on the decidability of expansions (Nat; <, P1, …, Pd) for various unary predicates P1, …, Pd. We focus in particular on predicates of arithmetic origin, such as Pow-k (powers of k) and N-k (k-th powers). The following is a representative sample of the results yielded by our techniques, which combine automata theory, algebra, number theory, dynamical systems, and combinatorics:

- The MSO theory of (Nat; <, Pow-2, Pow-3) is decidable.

- The MSO theory of (Nat; <, Pow-2, Pow-3, Pow-6) is decidable.

- The MSO theory of (Nat; <, Pow-2, Pow-3, Pow-5) is decidable subject to Schanuel's conjecture.

- The MSO theory of (Nat; <, Squares, Pow-4) is decidable.

- The MSO theory of (Nat; <; Squares, Pow-2) is Turing-equivalent to the MSO theory of (Nat; <, S), where S is the unary predicate corresponding to the binary expansion of s = sqrt(2). As s is widely believed to be a weakly normal number, the corresponding MSO theory is in turn expected to be decidable.

The talk will give an overview of our techniques in general, and the automata theory and algebra that enable the above results in particular.

La théorie des types et la théorie de l'homotopie
Vendredi 11 octobre 2024, 14 heures, Salle 1013
François Métayer Remarques sur le modèle simplicial de l’univalence, d’après Kapulkin-Lumsdaine-Voevodsky (I)

Dans ce premier exposé basé sur l’article « Univalence in simplicial sets » (https://arxiv.org/abs/1203.2553) je détaillerai la notion de « fibration universelle » qui en est l’ingrédient essentiel. J’examinerai en parallèle ce que devient une telle construction lorsqu’on remplace les ensembles simpliciaux par le cadre beaucoup plus simple des ensembles tout court.

Programmation
Lundi 14 octobre 2024, 10 heures, 4071
Pierre-Evariste Dagand (IRIF) A type-theoretic model of smart contracts

Smart contracts are programs that run on an interpreter cobbled together from a massively distributed network of mutually untrusting computers. Unsurprisingly, the unruly nature of the underlying execution engine has a profound impact on the behavior of the interpreter and thus the semantics of smart contracts.

Caught once again by my incurable curiosity, I have set out to delineate precisely what set smart contracts aside in the realm of programming languages.

This talk reports on some early results, modeling the semantics of smart contracts in a type-theoretic and monadic framework. The objective of this work is to support formal reasoning at the protocol level (that is, starting from a specification free from programming error).

We shall strive to stay on track and in good taste: the presentation will not cover any financial aspect of smart contracts.

Formath
Lundi 14 octobre 2024, 14 heures, 3052
Emilio Gallego Arias (Picube, IRIF) Non encore annoncé.