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. Tweets by IRIF_Paris Notion du jour Actualités 4.5.2023 Le pôle PPS organise ses journées 2023, les 25 et 26 mai prochains, et c'est ouvert à tous. 4.5.2023 Juliette Calvi, la nouvelle assistante de communication de l'IRIF est arrivée depuis la semaine dernière. N'hésitez pas à lui faire part de tous vos besoins en communication ou simplement à aller la rencontrer dans son bureau 4004. 15.5.2023 Congratulations to Jean Krivine (IRIF) and Vincent Danos (ENS and CNRS) who have received the Concur Test-of-Time Award (period 2002-2005) for their article “Reversible Communicating Systems”, published at CONCUR 2004. To read their article : 4.5.2023 Claire Mathieu a été citée dans un article du journal “La Croix” : “Intelligence artificielle : “pourquoi sa vision du monde est-elle si biaisée ?” 11.5.2023 À l’occasion du départ à la retraite de François Métayer, le LHC rendra hommage au spécialiste des polygraphes, de l’homotopie et de la réécriture, animateur d’un groupe de travail mythique sur ces sujets. L’événement aura lieu les *8 et 9 juin 2023 et sera précédé par les journées LHC 3.4.2023 We are proud to announce that Claire Mathieu was named as recipient of an EATCS fellowship for her fundamental contributions to solving theoretical and applied problems in approximation algorithms, online algorithms, and auction theory. 5.4.2023 The ANR CoREACT will have its kick-off on Wednesday 19 April. It will be in room 146 and online, open to everyone. Contact Nicolas Behr for the details. edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Combinatoire énumérative et analytique Jeudi 1 juin 2023, 11 heures, IHP Seminaire Flajolet Julien Courtiel, Anna Ben-Hamou, Christophe Hohlweg https://semflajolet.math.cnrs.fr/ Séminaire des membres non-permanents Jeudi 1 juin 2023, 16 heures, Olympe de Gouges 147 and Zoom link Thomas Colcombet Non encore annoncé. La syntaxe rencontre la sémantique Jeudi 1 juin 2023, 14 heures, salle 146 (Olympe de Gouges) Gabriele Vanoni (Univ. Bologna) Higher-Order and Non-Linear Bayesian Networks Catégories supérieures, polygraphes et homotopie Vendredi 2 juin 2023, 14 heures, salle 147 (Olympe de Gouges) Noam Zeilberger (LIX) Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem The classical statement of the Chomsky-Schützenberger representation theorem says that any context-free language may be represented as the homomorphic image of the intersection of a Dyck language of balanced parentheses with a regular language. In the talk I will discuss a fibrational perspective on context-free grammars and finite-state automata that grew out of a long-running project with Paul-André Melliès on type refinement systems, but with a surprising twist that only emerged when we considered the C-S theorem. It turns out that underlying that theorem is a basic adjunction between categories and colored operads (= multicategories), where the right adjoint $W : Cat \to Oper$ builds a “spliced arrow operad” out of any category, and the left adjoint $C : Oper \to Cat$ sends any operad to a “contour category” whose arrows have a geometric interpretation as oriented contours of operations. Based on joint work with Paul-André Melliès that appeared at MFPS 2022 (https://hal.science/hal-03702762), as well as a long version of that article in preparation. Automates Vendredi 2 juin 2023, 14 heures, Salle 146 Olympe de Gouges Alexandra Rogova ([DB]) GPC: A Pattern Calculus for Property Graphs Joint work with Nadime Francis, Amélie Gheerbrant, Paolo Guagliardo, Leonid Libkin, Victor Marsault, Wim Martens, Filip Murlak, Liat Peterfreund and Domagoj Vrgoč The development of practical query languages for graph databases runs well ahead of the underlying theory. The ISO committee in charge of database query languages is currently developing a new standard called Graph Query Language (GQL), the main component of which is the pattern matching facility. In many aspects, it goes well beyond RPQs, CRPQs, and similar queries on which the research community has focused for years. In this talk, I will present our distillation of the lengthy standard into a simple Graph Pattern Calculus (GPC) that reflects all the key pattern matching features of GQL. Graph Transformation Theory and Applications Vendredi 2 juin 2023, 15 heures, online Fernando Orejas (Department of Computer Science, Universitat Politècnica de Catalunya, Spain) Unification of Drags and Confluence of Drag Rewriting Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules. Zoom meeting registration link YouTube live stream Vérification Lundi 5 juin 2023, 11 heures, Olympe de Gouges 146 and Zoom link Pedro Ribeiro (University of York) Co-verification for robotics: simulation and verification by proof Robots are facilitating new business models from food delivery to healthcare. Current engineering practice cannot yet provide the formal guarantees needed to allay the safety concerns of regulators. Simulation, a technique favoured by practitioners, provides an avenue for experimenting with different scenarios before committing to expensive tests and proofs. In this talk, I will discuss how different models may be brought together for the (co-)verification of system properties, with simulation complementing formal verification. This will be explored in the context of the model-driven RoboStar framework, that clearly identifies models of the software, hardware, and scenario, and has heterogeneous formal semantics amenable to verification using model-checkers and theorem provers. Algorithmes et complexité Mardi 6 juin 2023, 11 heures, Salle 147 (Olympe de Gouges) Galina Pass (QuSoft, University of Amsterdam) (No) Quantum space-time tradeoff for USTCON Analyse et conception de systèmes Mercredi 7 juin 2023, 14 heures, Salle 146 (Olympe de Gouges) Samuel Vivien (ENS Paris, IRIF) How to prove that you need Cake ? PureCake, is a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. This talk will present how optimization soundness can be proven using equational reasoning with the example of the demand analysis pass and other related optimizations. Based on : PureCake: A Verified Compiler for a Lazy Functional Language [PLDI'23] by Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti Combinatoire énumérative et analytique Jeudi 8 juin 2023, 14 heures, Olympe de Gouges Davig Forge (Orsay) TBD