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 31.5.2023 Geoffroy Couteau et Pierre-Evariste Dagand ont écrit un texte à quatre mains dans le Blog Binaire du Journal Le Monde. Ils se demandent s'il est possible de contrôler l'accès aux sites pornographiques tout en conservant l'anonymat et les données de l'utilisateur pour protéger les enfants. C'est ici que le “zéro-proof knowledge” rentre en jeux… 4.5.2023 Le pôle PPS organise ses journées 2023, les 25 et 26 mai prochains, et c'est ouvert à tous. 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 : 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 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. 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. 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 ?” edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda 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. Formath Lundi 5 juin 2023, 14 heures, 146 (Olympe de Gouges) Wendlasida Ouedraogo (INRIA (Paris Saclay)) Source code optimization for safety critical systems A computer system is safety-critical when it can cause serious damage to property, the environment, human life, or to society as a whole. Real-world safety-critical systems are also necessarily complex, because, to take into account the interactions between software, hardware, the physical environment, and sometimes their distributed nature (systems of systems), they need to implement a variety of safety measures, in software, hardware, in the system design, at development time, at compile time, and at run-time. Those safety measures which vary from one safety-critical system to another very often lead to a decrease in performance, for a increase in the execution time of software. This research work is situated in the context of one such system, the communication-based train control (CBTC) system of Siemens Mobility France which operates a number of driverless subway systems around the World, including Paris lines 1, 4, and 14. That system is certified according to the industrial norm EN-50128 and up to the highest Safety Integrity Level 4, required for safety-critical systems with potentially catastrophic consequences. In this context, the thesis looks for an answer to the question of how to automatically optimize the execution time performance of such systems without losing the previously obtained safety guarantees. The answer provided is provably correct optimization of source code. A first contribution is a source-to-source compiler for VCP Ada (a subset of Ada) programs, that optimizes source code while preserving the formal semantics of the programs. The compiler has been proven correct in the Coq proof assistant and guarantees the equivalence of execution between the original and the optimized program. The compiler copes with the complexities of the platform, due to hardware safety measures, which is important, since real-world safety-critical systems are often susceptible to having such measures, potentially conflicting with existing formally proven optimizing compilers. Moreover, choosing the approach of a source-to-source compilation shows to have methodological advantages over an approach to proven optimizations having a number of intermediate languages, allowing to simplify and diminishing the needed proof effort. A second contribution is to the problem of provably correct lexical analysis of compilers, which has previously not received a lot of research attention, a weak link in any compilation chain using a proven or qualified compiler. We develop CoqLex, the first Coq-formalized lexer generator, based on a modification of an existing Coq implementation of regular expression matching via Brzozowski derivatives. The developed theory and tools have been applied to optimize real-world VCP Ada programs of CBTC systems, consisting of thousands of source files, with promising results. 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 The problem of undirected st-connectivity is important both for its applications in network problems, and for its theoretical connections with logspace complexity. Classically, a long line of work led to a time-space tradeoff of T=Õ(n^2/S) for any S such that S=Ω(log(n)) and S=O(n^2/m), where T is the running time and S is the used space. In this talk, I will present a surprising result that quantumly there is no nontrivial time-space tradeoff: there is a quantum algorithm that achieves both optimal time Õ(n) and optimal space O(log(n)) simultaneously. This improves on previous results, which required either O(log(n)) space and Õ(n^1.5) time, or Õ(n) space and time. To complement this, we show that there is a nontrivial time-space tradeoff when given a lower bound on the spectral gap of a corresponding random walk. 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 Séminaire des membres non-permanents Jeudi 8 juin 2023, 16 heures, Olympe de Gouges 147 and Zoom link Bernardo Jacobo-Inclan Non encore annoncé. Automates Vendredi 9 juin 2023, 14 heures, Salle 146 Olympe de Gouges Daniel Smertnig Deciding Sequential? and Unambiguous? for weighted automata over fields Previous work reduces the problem of deciding whether a weighted finite automaton (WFA) over a field is equivalent to a sequential, respectively, unambiguous, WFA to the computation of the linear hull. The linear hull is the topological closure of the reachability set in a certain linear version of the Zariski topology. We discuss an algorithm to compute the linear hull that works essentially entirely in the realm of linear algebra (i.e., without first resorting to the computation of the finer Zariski topology). Further, we show how this leads to double-exponential bounds on the size of the linear hull. This talk is on joint work with J. Bell. Vérification Lundi 12 juin 2023, 11 heures, Olympe de Gouges 146 and Zoom link Themistoklis Melissourgos (University of Essex) Non encore annoncé. Algorithmique distribuée et graphes Mardi 13 juin 2023, 15 heures, 147 Olympe de Gouges Anna Gujgiczer (Budapest University of Technology and Economics, Hungary) Circular chromatic number of generalised Mycielski graphs on odd cycles and other quadrangulations of the projective plane Generalised Mycielskians of odd cycles are relatively small graphs with high odd girth and chromatic number 4. In the literature there are many proofs using different techniques, like methods from algebraic topology, to show the second property. It is also proven by DeVos et al that these graphs have circular chromatic number 4. Using a result from about the same time of Simonyi and Tardos, namely that for a “topologically t-chromatic” graph $G$, where $t$ is even we have $\chi_c(G) = \chi(G) = t$, one can also get this strengthened statement. In this talk we present a new, relatively short direct proof for the circular chromatic number, using only a basic notion of algebraic topology, namely the winding number. Then we present another graph family with high odd girth and circular chromatic number 4. This construction is very similar to the generalized Mycielski, but on its first two layers it forms a M$\ddot{o}$bius ladder. We prove the statement about their circular chromatic number with similar techniques. Moreover we present a similar result for a family of signed graphs. This talk is based on a joint work with Reza Naserasr (Universit´e de Paris, IRIF, CNRS, F-75006, Paris, France), S Rohini (Indian Institute of Technology Madras, India) and S Taruni (Indian Institute of Technology Dharwad, India). Combinatoire énumérative et analytique Jeudi 15 juin 2023, 14 heures, Salle 146 - Olympe de Gouges Marc Noy (UPC (Espagne)) Chordal graphs with bounded tree-width https://arxiv.org/abs/2301.00194