Bienvenue 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. Notion du jour Réseaux Sociaux Suivez nous sur Mastodon, Twitter/X et LinkedIn : Actualités 18.10.2024 Nous souhaitons la bienvenue à Mélissa Goddé, nouvelle gestionnaire, qui vient renforcer l'équipe administrative. 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. 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. 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. 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. 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. 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. 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. edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Algorithmes et complexité Mardi 22 octobre 2024, 11 heures, Salle 3052 Adam Wesołowski (Royal Holloway) Advances in quantum algorithms for the shortest path problem In this talk, we will delve into quantum complexity of some graph problems: Single Pair Shortest Pathfinding (SPSP), Diameter, Radius, Eccentricity. We will shortly review the electrical network framework for graphs and proceed to discuss recent advances in quantum algorithms and lower bounds for these problems and present a number of open problems. We give an algorithm in the adjacency array model that under special conditions solves the SPSP problem in $\tilde{O}(l\sqrt{m})$ steps, and with parallelization in $\tilde{O}(\sqrt{lm})$ steps, matching the upper bound on path detection up to polylog factors, where $l$ is the length of the shortest path between the considered vertices. Combinatoire énumérative et analytique Jeudi 24 octobre 2024, 14 heures, Salle 3071 Mark Skandera [jour et heure inhabituels!] Une généralisation de la formule des défauts de Deodhar pour la multiplication des éléments de base de Kazhdan-Lusztig Soit H l'algèbre de Hecke d'un groupe de Coxeter (W,S). En étudiant la base Kazhdan-Lusztig de H, Deodhar a considéré les produits C_{w^{(1)} *…* C_{w^{(k)}, où (w^{(1)},… ,w^{(k)}) est une séquence de générateurs dans S. Il a défini et a compté certains “défauts” de telles séquences pour exprimer les produits correspondants dans la base naturelle de H. Nous étendons sa définition à des séquences d'éléments plus généraux de W et exprimons ainsi des produits plus généraux dans la base naturelle de H, dans la cas où W est de type A ou BC. Ce travail a été réalisé en collaboration avec Gavin Hobbs, Tommy Parisi, et Jiayuan Wang. Preuves, programmes et systèmes Jeudi 24 octobre 2024, 10 heures 30, Salle 3052 & online (Zoom link) Jean-Jacques Lévy (Inria) Tracking Redexes in the lambda-calculus Redexes have residuals and can create new redexes in the (typed or untyped) lamda-calculus. We will review these basic notions which are at the heart of strong normalization and reduction strategies. This talk deals with permutation equivalence, residuals modulo permutations, redex families, the labeled lambda-calculus, general finite developments and optimal reductions. The talk is a revised version of an article published in the book “The French School of Programming”, Springer, 2024. Séminaire des membres non-permanents Jeudi 24 octobre 2024, 16 heures, Room 3052 Avinandan Das (PhD Student) Fooling around with Graphs : Forcing Alice and Bob to make mistakes to prove communication lower bounds. We are in the 2-party communication setup which is as follows. There are two players Alice and Bob who are given as inputs, graphs G_1 and G_2 respectively. They communicate with each other to compute some function f on the graph G_1 \cup G_2. How many bits of communication are required between them in order for them to compute the function f ? In this technique, we will first set up the communication model, consider graph problems like maximum matching, degeneracy and coloring in this model and then delve into the technique of fooling sets in order to arrive to communication bandwidth lower bounds for these problems in the two party set-up. Fooling set is a mechanism to design inputs for Alice and Bob such that if too few bits are communicated between them, then both of them are ``fooled'' into making mistakes. If time permits, we will also peek into the mechanism of proving lower bounds for problems in streaming model using communication lower bounds. Automates Vendredi 25 octobre 2024, 14 heures, Salle 3052 Isa Vialard Measuring well quasi-orders Well quasi orderings (WQOs) are at the heart of the theory of Well-Structured Systems (WSTS), a class of computational models that brought numerous important advances for the automatic verification of infinite-state systems. Recent developments in this field links the complexity of WQO-based algorithms to ordinal measures of WQOs : the maximal order type, ordinal height and ordinal width. One main challenge is to compute the ordinal invariants of complex well quasi-orders built from simpler well quasi-orders through classical operation, such as the Cartesian product, and high-order constructions, like the finite words embedding. In my thesis, I computed compositionally the maximal order type of the direct product, the width of the multiset embedding, and the height and width of the multiset ordering. Furthermore, I compute the width of the Cartesian product in restricted cases and studied the ordinal measures of the finite powerset.In the process, I developed several tools and techniques, notably a game-theoretical approach to computing width using the notion of quasi-incomparable families of subsets. To tackle the width of the multiset ordering, I introduced and studied a fourth ordinal invariant, the friendly order type. One world numeration seminar Mardi 29 octobre 2024, 14 heures, Online Victor Shirandami (University of Manchester) Probabilistic Effectivity in the Subspace Theorem and the Distribution of Algebraic Projective Points The celebrated Roth’s theorem in Diophantine Approximation determines the degree to which an algebraic number may be approximated by rationals. A corollary of this theorem yields a transcendence criterion for real numbers based off of their decimal expansion. This theorem, and its broad generalisation due to Schmidt, famously suffers from ineffectivity. This motivates one to address this issue in the probabilistic context, whereby one makes progress in the direction of effectivity in an appropriately defined probabilistic regime. From this analysis is derived an analogue of Khintchine's theorem for algebraic numbers, answering a question of Beresnevich, Bernick, and Dodson on a density version of Waldschmidt’s conjecture. Programmation Lundi 4 novembre 2024, 10 heures, 3071 Thierry Martinez (INRIA) Coq Deep Pattern-Matching using Small Inversion I will present joint work with Pierre Boutillier, Hugo Herbelin, and Meven Lennon-Bertrand. We are implementing a new algorithm, described in Pierre's PhD thesis and further developed during Meven's internship, for pattern-matching elaboration in Coq. This algorithm starts from a richer form of pattern-matching than what is currently available by default in Coq, handling deep and multiple pattern-matching with dependent types, as proposed by Thierry Coquand in the 1990s, while targeting the same elementary form of pattern-matching present in the Coq kernel. Most of the design challenges for this algorithm come from handling the equalities that appear at each level of deconstruction of dependent inductive values. I will compare three approaches: one proposed by Healfdene Goguen, Conor McBride, and James McKinna, which relies on the equivalence axiom between homogeneous and heterogeneous equalities (equivalent to the Uniqueness of Identity Proofs); a refinement proposed by Jesper Cockx, which avoids the need for axioms; and the encoding by small inversion, which moves the proofs of deconstruction of the dependencies from the term level to the type level. While these algorithms give an encoding of dependent pattern-matching into the Coq kernel, this discussion leads us to think about what could be a better primitive form of pattern-matching. Combinatoire énumérative et analytique Mardi 5 novembre 2024, 14 heures, Salle 3071 Hugo Manet [heure inhabituelle!] tba Sémantique Mardi 5 novembre 2024, 15 heures, Salle 3071 Louis Lemonnier (University of Edinburgh) A recipe for the semantics of reversible programming In this presentation, we explore the foundational elements required to interpret reversible programming within a categorical framework. We use the symmetric pattern-matching language introduced by Sabry, Valiron, and Vizzotto as a reference point, and we incorporate several improvements. We show that inductive data types and recursion can also be effectively modelled in this setting. However, these results do not straightforwardly extend to the pure quantum case. We provide insights into the challenges encountered and propose potential directions for addressing these limitations, for example with guarded recursion. (Self) references: Classical reversible semantics: https://doi.org/10.4230/LIPIcs.FSCD.2024.19 / https://arxiv.org/abs/2309.12151 First-order quantum semantics (chapter 3): https://theses.hal.science/tel-04625771 / https://arxiv.org/abs/2406.07216 Non-cartesian guarded recursion: https://arxiv.org/abs/2409.14591 Automates Vendredi 8 novembre 2024, 14 heures, Salle 3052 Benjamin Bordais Non encore annoncé.