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 LinkedIn, Bluesky et Mastodon : Actualités 14.3.2025 Le troisième épisode du podcast “Qu'est ce que tu cherches ?” du CNRS a invité Geoffroy Couteau pour parler de son sujet de recherche : la protection des données privées, les calculs sécurisés, les protocoles sécurisés. Vous pourrez également découvrir sa journée type, le moment où il fait le plus de sciences (et non, ce n'est pas forcément pendant la journée !), les stéréotypes liés à son domaine. (Ré)Écoutez cet épisode : 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 12 mai 2025, 11 heures, 3052 and Zoom link Jeroen Keiren (Eindhoven University of Technology) An Expressive Timed Modal Mu-Calculus for Timed Automata In the untimed setting, it is well-known that the modal mu-calculus is more expressive than other modal logics such as LTL, CTL and CTL*. It can thus be considered a foundational logic for model-checking. In the timed setting, the status of similarly foundational logics is less satisfactory. There are timed extensions of modal logics, such as TCTL. Yet, the state of the art of timed mu-calculi is underdeveloped. In this talk, I present a timed model mu-calculus $L_{rel}^{\mu,\nu}$ for encoding properties of systems modeled as timed automata. Our logic includes arbitrary fixpoints and an until-like modal operator for time elapses, and is shown to be strictly more expressive than existing timed modal mu-calculi introduced in the literature. It also enjoys decidable model checking, as it respects the traditional region-graph construction for timed automata. Additionally, I establish that, in contrast to other timed mu-calculi, $L_{rel}^{\mu,\nu}$ is strictly more expressive than Timed Computation Tree Logic (TCTL) in the setting of general timed automata, meaning that model checkers for $L_{rel}^{\mu,\nu}$ are immediately usable as model checkers for TCTL for general timed automata. This is joint work with Rance Cleaveland and Peter Fontana, and appeared as [1]. [1] Cleaveland, R., Keiren, J.J.A., Fontana, P.: An Expressive Timed Modal Mu-Calculus for Timed Automata. In: Hillston, J. et al. (eds.) Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems., pp. 160–178. Springer Nature Switzerland, Cham (2024). Formath Lundi 12 mai 2025, 14 heures, 3052 Collectif Discussion suivant le cours de Thierry Coquand One world numeration seminar Mardi 13 mai 2025, 14 heures, Online Artem Dudko (IM PAN) On attractors of Fibonacci maps In 1990s Bruin, Keller, Nowicki, and van Strien showed that smooth unimodal maps with Fibonacci combinatorics and sufficiently high degree of a critical point have a wild attractor, i.e. their metric and topological attractors do not coincide. However, until now there were no reasonable estimates on the degree of the critical point needed. In the talk I will present an approach for studying attractors of maps, which are periodic points of a renormalization. Using this approach and rigorous computer estimates, we show that the Fibonacci map of degree $d=3.8$ does not have a wild attractor, but that for degree $d=5.1$ the wild attractor exists. The talk is based on a joint work with Denis Gaidashev. Preuves, programmes et systèmes Mercredi 14 mai 2025, 10 heures, Salle 3071 Joachim Kock (UAB Barcelona & U Copenhagen) Lectures on Decomposition Spaces The theory of decomposition spaces arose out of a need for a more flexbible framework for incidence (co)algebras and Möbius inversion than the classical setting of locally finite posets. As the name suggests, it is a theory of decomposition rather than composiition (as in categories), and it appears that all combinatorial coalgebras are incidence coalgebras of a decomposition space (whereas many of them cannot be realised directly as the incidence coalgebra of any poset). The lectures will be an introduction to decomposition spaces from the viewpoint of combinatorics, but the tools come from category theory and simplicial homotopy theory. The first lecture will start with a brief review of the classical Möbius functioin in number theory, and Rota's theory for locally finite posets. Here the notion of reduction is important: often it has the flavour of cooking up an auxiliary poset in order to apply the classical theory, and then impose an equivalence relation so as to arrive at the coalgebra actually needed. With this motivation, we then move on to Möbius categories and decomposition spaces, and go through some examples beyond posets, such as the chromatic Hopf algebra of graphs and the Butcher-Connes-Kreimer Hopf algebra of rooted trees. The second lecture will be a bit more categorical, including an introduction to objective algebraic combinatorics using objective linear algebra: this is linear algebra with coefficients in sets and groupoids instead of number coefficients. Slice categories play the role of vector spaces, and linear functors (given by spans) play the role of linear maps. By working at this level, the theory of decomposition spaces can be seen as a systematic way of lifting coalgebraic identities to 'bijective proofs'. I'll spend some time explaining the need for groupoids and homotopy theory, exemplified with the Faà di Bruno bialgebra. The third lecture focuses on functorialities, explaining how certain simplicial maps called CULF and IKEO induce coalgebra homomorphisms. Especially important is the simplicial notion of decalage, which underlies many of the reductions in classical theory. CULF maps also enter in the definition of monoidal decomposition spaces, in turn inducing bialgebras and Hopf algebras (rather than just coalgebras). I hope to be able to finish with some potential applications to process calculi and quantum logic. Sometimes processes cannot be composed, or can be composed in many ways. Often this means there is instead a well-defined decomposition operation, and likely a decomposition space. Similarly, effect algebras and effect algebroids describe situations where composition is only partially defined, with axioms ensuring that they are in fact examples of decomposition spaces. Zoom meeting link Algorithmes et complexité Mercredi 14 mai 2025, 11 heures, Salle 3052 Youlong Ding (The Hebrew University of Jerusalem) A New Approach to LPN-Based Pseudorandom Functions: Low-Depth and Key-Homomorphic We give new constructions of pseudorandom functions (PRFs) computable in NC1 from (variants of the) Learning Parity with Noise (LPN) assumption. Prior to our work, the only NC1-computable PRF from LPN-style assumptions was due to Boyle et al. (FOCS 2020) who constructed a weak PRF from a new heuristic variant of LPN called variable-density LPN. We give the following three results: 1. A weak PRF computable in NC1 from standard LPN. 2. A (strong) encoded-input PRF (EI-PRF) computable in NC1 from sparse LPN. An EI-PRF is a PRF whose input domain is restricted to an efficiently sampleable and recognizable set. The input encoding can be computed in NC1+eps for any constant eps, implying a strong PRF computable in NC1+eps. 3. A (strong) PRF computable in NC1 from a (new, heuristic) seeded LPN assumption. As a bonus, all of our PRF constructions are key-homomorphic, an algebraic property that is useful in many symmetric-cryptography applications. No previously-known LPN-based PRFs are key-homomorphic, even if we completely ignore depth-efficiency. In fact, our constructions support key homomorphism for linear functions (and not only additive), a property that no previously-known PRF satisfies, including ones from LWE. Technically, all of our constructions leverage a new recursive derandomization technique for LPN instances, which allows us to generate LPN error terms deterministically. This technique is inspired by a related idea from the LWE literature (Kim, EUROCRYPT 2020) for which devising an LPN analogue has been an outstanding open problem. Théorie des Topos Mercredi 14 mai 2025, 14 heures, Salle 3052 Miriam Marzaioli Forcing and topos theory (chapter VI) Séminaire des membres non-permanents Jeudi 15 mai 2025, 16 heures, Salle 3052 Lucas Pouillart Coxeter systems or the story of combinatorics on words in reflection groups Reflection groups have been studied for a really long time for their geometry and combinatorics as automorphism groups of regular polyhedrons and have not ceased to appear in many areas of mathematics and computer science such as representation theory, graph theory ever since. In this talk we will try to explain the general structure of a reflection group by looking at their word problem.“ Automates Vendredi 16 mai 2025, 14 heures, Salle 3052 Lê Thành Dũng (Tito) Nguyễn (LIS (Marseille)) The structure of polynomial growth for tree automata/transducers and MSO set queries Given an ℕ-weighted tree automaton, we give a decision procedure for exponential vs polynomial growth (with respect to the input size) in quadratic time, and an algorithm that computes the exact polynomial degree of growth in cubic time. As a special case, they apply to the growth of the ambiguity of a nondeterministic tree automaton, i.e. the number of distinct accepting runs over a given input. Our time complexities match the recent fine-grained lower bounds for these problems restricted to ambiguity of word automata. We deduce analogous decidability results (ignoring complexity) for the growth of the number of results of set queries in Monadic Second-Order logic (MSO) over ranked trees. In the case of polynomial growth of degree k, we also prove a reparameterization theorem for such queries: their results can be mapped to k-tuples of input nodes in a finite-to-one and MSO-definable fashion. This has several consequences for transducers, that I will probably not have the time to cover in the talk, but you can check out the preprint: https://arxiv.org/abs/2501.10270 (joint work with Paul Gallot and Nathan Lhote). Formath Lundi 19 mai 2025, 14 heures, 3052 et en visio François Lamarche La topologie algébrique et la géométrie peuvent faire de nouvelles contributions à la théorie des types dépendants, en plus du concept d'univalence. Formath Lundi 19 mai 2025, 15 heures, 3052 et en visio Collectif Discussion informelle après le cours de Thierry Coquand