image/svg+xml Bienvenue L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université de Paris, 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), cinq 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 18.1.2022 Two papers coauthored by IRIF members will be presented at the 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022) held in Marseille, March 15-18 2022. 29.11.2021 IRIF has the great pleasure to welcome a new professor in computer science at Université de Paris: Matěj Stehlík, an expert in graph theory. Learn more about him and his work here. 17.12.2021 Paul-André Melliès (IRIF), Arthur Vale, Zhong Shao, Jérémie Koenig (Yale) and Léo Stefanesco (MPI) will present a layered concurrent object-based game semantics for the purpose of compositional software specification and certification at annual Symposium on Principles of Programming Languages, POPL2022 : https://hal.inria.fr/hal-03456034. 13.12.2021 Delia Kesner (IRIF) will present her paper A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-Nets at annual Symposium on Principles of Programming Languages, POPL2022. The paper introduces a functional term calculus that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. 2.12.2021 IRIF is very pleased to host for two months Serge Massar, Professor at the Université libre de Bruxelles (ULB) as part of the FSMP Distinguished Professor Fellowship. Serge Massar is the director of the Laboratoire d'Information Quantique (LIQ), of the Physics Department, Science Faculty, ULB. His research interests are quantum information theory, experimental quantum and non linear optics, machine learning. 13.12.2021 Jacques Sakarovitch (IRIF) was elected new IFIP Fellow. IFIP Fellow is the most most prestigious IFIP's technical distinction which is conferred by the IFIP General Assembly on a current or past member of an IFIP body in recognition of outstanding contributions in the field of information processing, in the role of a Technical Leader, Scientist, Engineer, or Educator. 1.12.2021 Prochaine conférence dans le cadre des 75 ans d’informatique : L’informatique dans le 7ème art : fiction ou réalité ? Rendez-vous avec Fabrice Kordon le jeudi 9 décembre-18h00 sur le campus Pierre et Marie Curie de Sorbonne Université (tour 25.26, 1er étage – salle 105). 2.12.2021 We are excited to be part of the “High-Performance Computer and Quantum Simulator hybrid” (HPCQS) aiming at creating a world-class supercomputing ecosystem. Learn more about the project here. edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Automates Vendredi 28 janvier 2022, 14 heures 30, Salle 3052 Soumyajit Paul Complexity of solving extensive form games with imperfect information n games with Imperfect information players only have partial knowledge about their position in the game. This makes the task of computing optimal strategies hard especially when players forget previously gained information. To further substantiate this hardness we consider two player zero-sum games with imperfect information modeled in the extensive form and provide several new complexity results on computing maxmin value for various classes of imperfect information. For these lower bound results we consider problems such as the Square-root sum problem and also complexity classes which involve computation over reals, more precisely Existential Theory of Reals (ETR) and other fragments of the First Order Theory of Reals (FOT(R)). This is joint work with Hugo Gimbert and B. Srivathsan. Graph Transformation Theory and Applications Vendredi 28 janvier 2022, 15 heures, online William Waites (University of Strathclyde, Scotland, UK) Rule-based Models of Epidemics Rule-based models, a particular kind of graph rewriting system initially intended for use in molecular biology, are conspicuously useful for understanding epidemics. They enable formulation of complex processes that blends the ease of understanding of “compartmental” models with the expressiveness of individual- or agent-based models. We illustrate this with a story, told in graph rewriting rules, of how the adaptive immune response to a pathogen works (simplified version) and how this response influences the population level dynamics of an epidemic. This model can be calibrated against real-world data and we see how some of the individual heterogeneity that is normally treated phenomenologically in the study of epidemics arises naturally from this account of immune response. Zoom meeting registration link YouTube live stream Vérification Lundi 31 janvier 2022, 11 heures, Zoom link Corto Mascle (LABRI) Responsibility and verification: Importance value in temporal logics We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case. One world numeration seminar Mardi 1 février 2022, 14 heures 30, Online Jonas Jankauskas (Vilniaus universitetas) Digit systems with rational base matrix over lattices Let $A$ be a matrix with rational entries and no eigenvalue in absolute value smaller than 1. Let $\mathbb{Z}^d[A]$ be the minimal $A$-invariant $\mathbb{Z}$-module, generated by integer vectors and the matrix $A$. In 2018, we have shown that one can find a finite set $D$ of vectors, such that each element of $\mathbb{Z}^d[A]$ has a finite radix expansion in base $A$ using only the digits from $D$, i.e. $\mathbb{Z}^d[A]=D[A]$. This is called 'the finiteness property' of a digit system. In the present talk I will review more recent developments in mathematical machinery, that enable us to build finite digit systems over lattices using reasonably small digit sets, and even to do some practical computations with them on a computer. Tools that we use are the generalized rotation bases with digit sets that have 'good' convex properties, the semi-direct ('twisted') sums of such rotational digit systems, and the special, 'restricted' version of the remainder division that preserves the lattice $\mathbb{Z}^d$ and can be extended to $\mathbb{Z}^d[A]$. This is joint work with J. Thuswaldner, “Rational Matrix Digit Systems”, to appear in “Linear and Multilinear Algebra” (arXiv preprint: https://arxiv.org/abs/2107.14168). Combinatoire énumérative et analytique Jeudi 3 février 2022, 14 heures, IHP Amphi Darboux Seminaire Flajolet Jiang Zeng et Marie Albenque http://semflajolet.math.cnrs.fr/index.php/Main/HomePage Automates Vendredi 4 février 2022, 14 heures 30, Salle 3052 (Online) Bartek Klin Orbit-finite-dimensional vector spaces, with applications to weighted register automata I will discuss vector spaces spanned by orbit-finite sets. These spaces are infinite-dimensional, but their sets of dimensions are so highly symmetric that the spaces have many properties enjoyed by finitely-dimensional spaces. Applications of this include a decision procedure for equivalence of weighted register automata, which are the common generalization of weighted automata and register automata for infinite alphabets. The algorithm runs in exponential time, and in polynomial time for a fixed number of registers. As a special case, we can decide, with the same complexity, language equivalence for unambiguous register automata. (Joint work with Mikołaj Bojańczyk and Joshua Moerman.) One world numeration seminar Mardi 8 février 2022, 14 heures 30, Online Magdaléna Tinková (České vysoké učení technické v Praze) Universal quadratic forms, small norms and traces in families of number fields In this talk, we will discuss universal quadratic forms over number fields and their connection with additively indecomposable integers. In particular, we will focus on Shanks' family of the simplest cubic fields. This is joint work with Vítězslav Kala. Combinatoire énumérative et analytique Jeudi 10 février 2022, 14 heures, Salle 1007 Daniel Tamayo Permutree Sorting We define permutree sorting which generalizes the stack sorting and Coxeter sorting algorithms respectively due to Knuth and Reading. Given two disjoint subsets U and D of {2,…,n}, it consists of an algorithm that fails for a permutation if and only if there are integers i<j<k in [n] such that the permutation contains the pattern jki (resp. kij) if j is in U (resp. in D). We present this algorithm through automata that read reduced expressions and accept only those that form a specific structure within the weak order. This is joint work with Vincent Pilaud and Viviane Pons. Analyse et conception de systèmes Vendredi 11 février 2022, 10 heures 30, Salle 3002 Denis Merigoux (Inria Paris) Hacspec: succinct, executable, verifiable specifications for high-assurance cryptography embedded in Rust Despite significant progress in the formal verification of security-critical components like cryptographic libraries and protocols, the secure integration of these components into larger unverified applications remains an open challenge. The first problem is that any memory safety bug or side-channel leak in the unverified code can nullify the security guarantees of the verified code. A second issue is that application developers may misunderstand the specification and assumptions of the verified code and so use it incorrectly. In this presentation, we propose a novel verification framework that seeks to close these gaps for applications written in Rust. At the heart of this framework is hacspec, a new language for writing succinct, executable, formal specifications for cryptographic components. Syntactically, hacspec is a purely functional subset of Rust that aims to be readable by developers, cryptographers, and verification experts. An application developer can use hacspec to specify and prototype cryptographic components in Rust, and then replace this specification with a verified implementation before deployment. We present the hacspec language, its formal semantics and type system, and describe a translation from hacspec to F*. We evaluate the language and its toolchain on a library of popular cryptographic algorithms. Graph Transformation Theory and Applications Vendredi 11 février 2022, 15 heures, online Pablo Arrighi (Université Paris-Saclay, France) Quantum Causal Graph Dynamics Suppose that an entire graph evolves quantum mechanically and gets driven into superpositions of graphs of different connectivities and node populations. Suppose moreover that the evolution is causal, meaning that information can only propagate at a bounded speed, with respect to graph distance. We show that this quantum evolution must decompose into small, local unitary rewritings of graph disks. This unifies a result on Quantum Cellular Automata with another on Reversible Causal Graph Dynamics. To reach the result we formalize a notion of causality which is valid in the context of quantum superpositions of time-varying graphs, and has a number of good properties. References: 1, 2, 3 Zoom meeting registration link YouTube live stream