Bienvenue L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, qui 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. Six 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 Twitter/X et LinkedIn pour suivre toute notre actualité : Actualités 27.9.2023 Grâce au travail d'Alexandra Rogova, l'équipe Automates et applications de l'IRIF, en association avec plusieurs équipes externes s'intéressant à la théorie des bases de données (au LIGM, l'ENS, Telecom Paris, etc.), relance le site et la newsletter de « Database Theory in Paris », qui centralise les évènements scientifiques de cette thématique en région parisienne. 5.9.2023 Toutes nos félicitations à Amélie Gheerbrant, maîtresse de Conférences, qui vient d'être nommée Vice-Doyenne (VD) Vies des campus et Vie étudiante au sein de l'Université Paris Cité ! 11.9.2023 IRIF is back to school! Today, we are welcoming our 12 new permanent members to our laboratory. As part of this day, they will present their research topics to us. 14.9.2023 Après avoir eux-mêmes suivis la Fresque du Climat, des membres du laboratoire de l'IRIF formeront, en tant que facilitateurs, des élèves de L1 à la Fresque du Numérique vendredi 15 septembre. Cet atelier permet de comprendre en équipe et de manière ludique les enjeux environnementaux du numérique. 6.9.2023 L'IRIF est très fier d'annoncer que Geoffroy Couteau, chargé de recherche du CNRS, a obtenu un financement pour son projet ERC Starting Grant : “Overcoming Barriers and Efficiency Limitations in Secure Computation”. Pour en savoir plus sur son projet et ses ambitions : 11.9.2023 Congratulations to Mohammed Foughali, who has published a paper titled “Compositional Verification of Embedded Real-Time Systems”, alongside Pierre-Emmanuel Hladik from Nantes Université/LS2N and Alexander Zuepke from the Technical University of Munich in the Journal of Systems Architecture. You can access the article here: edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Formath Lundi 2 octobre 2023, 14 heures 15, 3052 SG Emilio Gallego Arias (IRIF & PICUBE, INRIA) Flèche: Incremental Validation for Hybrid Formal Documents We present Flèche, an engine for the incremental validation and edition of scientific formalized documents. Flèche provides a formal document model, based on a notion of functional interpretation for a family of languages plus algebraic effects capturing document dynamics. Flèche targets existing systems with non-trivial interfaces and documents in their daily use. Some features of Flèche are: a) hybrid formal documents, where natural language is intermixed with its formal counterpart; b) modular error recovery and handling of incomplete documents; c) incremental, full-project model; d) standard document edition workflow. We have released a Flèche implementation for the Coq Proof Assistant, `coq-lsp`, that uses the Language Server Protocol (LSP) as an editor API. Together with LSP-capable editors like Visual Studio Code, `coq-lsp` provides a new user interface for the Coq system with unique characteristics. Combinatoire énumérative et analytique Mardi 3 octobre 2023, 11 heures, Salle 1007 Éric Fusy (CNRS & LIGM, Université Gustave Eiffel) Énumération de rectangulations Je présenterai des résultats sur l'énumération exacte et asymptotique de rectangulations génériques (partitions d'un rectangle en régions rectangulaires, sans point où 4 rectangles se rencontrent, et considérées selon deux relations d'équivalences, faible ou forte). Ces objets sont en correspondance avec certains modèles de cartes planaires orientées (orientations bipolaires dans le cas faible, structures transverses dans le cas fort), qui peuvent être encodées par certains chemins dans le quart de plan en appliquant une bijection due à Kenyon, Miller, Sheffield et Wilson. Je montrerai également une extension au cas de rectangulations non génériques, donnant un continuum de modèles de cartes planaires aléatoires qui s'approchent asymptotiquement du réseau régulier. Travaux en commun avec Erkan Narmanli et Gilles Schaeffer Algorithmes et complexité Mardi 3 octobre 2023, 11 heures, Salle 3052 Marcos Kiwi (Universidad de Chile) Label propagation on binomial random graphs We study a variant of the widely popular, fast, and often used family of community detection procedures referred to as label propagation algorithms. These mechanisms also exhibit many parallels with models of opinion exchange dynamics and consensus mechanisms in distributed computing. Initially, given a network, each vertex starts with a random label in the interval [0,1]. Then, in each round of the algorithm, every vertex switches its label to the majority label in its neighborhood (including its own label). At the first round, ties are broken towards smaller labels, while at each of the next rounds, ties are broken uniformly at random. We investigate the performance of this algorithm on the binomial random graph G(n,p). Via a technically delicate analysis, we show that for np>n^(5/8+epsilon), the algorithm terminates with a single label a.a.s. Moreover, we show that if np = omega(n^(2/3)), a.a.s., this label is the smallest one, whereas if n^(5/8+epsilon) < np = o(n^(2/3)), the surviving label is, a.a.s., not the smallest one. Joint work with Lyuben Lichev (Univ. Jean Monnet), Dieter Mitsche (Univ. Jean Monnet & Pontifícia Univ. Católica de Chile), and Pawel Pralat (Toronto Metropolitan Univ.). One world numeration seminar Mardi 3 octobre 2023, 14 heures, Online Manfred Madritsch (Université de Lorraine) Construction of absolutely normal numbers Let $b\geq2$ be a positive integer. Then every real number $x\in[0,1]$ admits a $b$-adic representation with digits $a_k$. We call the real $x$ simply normal to base $b$ if every digit $d\in\{0,1,\dots,b-1\}$ occurs with the same frequency in the $b$-ary representation. Furthermore we call $x$ normal to base $b$, if it is simply normal with respect to $b$, $b^2$, $b^3$, etc. Finally we call $x$ absolutely normal if it is normal with respect to all bases $b\geq2$. In the present talk we want to generalize this notion to normality in measure preserving systems like $\beta$-expansions and continued fraction expansions. Then we show constructions of numbers that are (absolutely) normal with respect to several different expansions. Sémantique Mercredi 4 octobre 2023, 10 heures 45, Salle 3052, 3ème étage du bâtiment Sophie Germain Ryan Kavanagh (McGill University) Stable Semantics for Recursive Session-Typed Processes Session-typed programming languages help programmers correctly implement communicating systems. Though many techniques exist for reasoning about these languages and their processes, few treat general recursive types and few are compositional. As a consequence, they cannot be applied to many useful programs and they do not support modular reasoning. In this talk, I will present a denotational semantics for Polarized Intuitionistic Processes (PIP), a session-typed proofs-as-processes interpretation of polarized intuitionistic linear logic. PIP features general recursion, channel transmission, choices, and synchronization. This semantics generalizes Kahn’s semantics for dataflow networks to support bidirectional, session-typed communication. It supports modular reasoning and validates expected program equivalences. Moreover, it is sound relative to barbed congruence (the canonical behavioural notion of process equivalence), and it is fully abstract in the absence of negative channel transmission. As a result, our semantics provides an intuitively reasonable account of session-typed communication and a foundation for reasoning about processes in more realistic session-typed languages. Analyse et conception de systèmes Jeudi 5 octobre 2023, 14 heures, salle séminaire, plateau Scai, 1er étage, Bâtiment Esclangon (Jussieu) Théo Zimmermann (LTCI, Télécom Paris, Institut Polytechnique de Paris) Une théorie des organisations communautaires de maintenance de paquets Dans de nombreux écosystèmes de langages de programmation, les développeurs dépendent de plus en plus de dépendances externes en open source, disponibles via des gestionnaires de paquets. Les paquets clés qui ne sont pas maintenus présentent un risque pour les projets qui en dépendent ainsi que pour les écosystèmes. Par conséquent, des initiatives communautaires peuvent émerger au sein des écosystèmes pour résoudre ce problème en adoptant les paquets clés ayant des problèmes de maintenance. Dans mon exposé, je présenterai les résultats de l'article coécrit avec Jean-Rémy Falleri et récemment publié dans Empirical Software Engineering intitulé “A Grounded Theory of Community Package Maintenance Organizations”. Le but de celui-ci était de construire une théorie de ces organisations (CPMO), notamment leur émergence et leur mode de fonctionnement. Pour ce faire, nous avons utilisé une méthodologie qualitative appelée Grounded Theory. Nous avons analysé des documents existants provenant de plusieurs CPMO, tels que des documentations et des discussions sur des forums publics, complétés par des entretiens avec des initiateurs de CPMO. Je parlerai également de mon application de ce modèle d'organisation à l'écosystème Coq, avec la création de l'organisation Coq-community, et de l'expérience acquise par ce biais. Automates Vendredi 6 octobre 2023, 14 heures, Salle 3052 Christian Choffrut Synchronous orders on the set of integers End of july 2023 Jeff Shallit asked me the following question: assuming that a synchronous automaton (two tapes read simultaneously) recognizes an ordering on the free monoid, is it decidable whether or not this ordering has infinite chains? infinite antichains? and questions of the like. I suspect(ed) that this is not the case but I started to work in the special unary case (the alphabet has a unique letter). I proved that these questions are decidable (it's easy), I characterized the orders that are linear and showed that the equivalence of two linear orders is polynomial (more interesting). I posted it on arxiv on september 19. Then I thought that I should enrich my introduction … and found out that these were (very) old results. The characterization of linear synchronous orderings on the integers is mentioned in a paper of Liu and Minnes (2009), which refers to a paper of Khoussainov and Rubin (2001) where it is implicit and is obtained as a general result on unary relations (not necessarily orderings). In my talk I will also comment on these results and propose some possible (hopefully genuinely novel!) extensions. Graph Transformation Theory and Applications Vendredi 6 octobre 2023, 15 heures, online Ryan Wisnesky (Conexus AI, San Francisco, California, USA) Functorial Data Migration In this talk we describe functorial data migration from a re-writing perspective, by way of the open-source CQL tool from categoricaldata.net. We describe how co-presheaves and their lifting problems can be finitely presented, how solving word problems in categories enables computational category theory, and some techniques for performing functorial data migration using chase algorithms. Zoom meeting registration link YouTube live stream Vérification Lundi 9 octobre 2023, 11 heures, 3052 and Zoom link Emily Clément (IRIF) Layered controller synthesis for dynamic multi-agent systems. We present a layered method to solve a multi-agent state problem, involving Timed Automata, SMT and Reinforcement Learning. The first layer of our method, based on Timed Automata, efficiently models the systems and gives us a high-level plan. Then, in a second step, we refine our model and solve it with SMT. We combining these steps and call it the SWA-SMT solver. A main issue is that it cannot be executed in real time. To overcome this, we use SWA-SMT solutions as the initial training dataset for our final step, which aims to obtain a neural network control policy. We use reinforcement learning to train the policy. We develop and show an example where the use of this initial dataset is crucial for the overall success of the method. Combinatoire énumérative et analytique Mardi 10 octobre 2023, 11 heures, Salle 381F du bâtiment Halles aux farines (ATTENTION!) Vincent Jugé (LIGM, en délégation à l'IRIF) TBA (ATTENTION exceptionnellement en salle 381F bâtiment Halles aux farines!)