www.irif.fr Open in urlscan Pro
2001:660:3301:9243::51c2:1bab  Public Scan

Form analysis
0 forms found in the DOM

Text Content

 * INFORMATIONS
   * Présentation
   * Contacts et accès
   * Charte des membres de l’IRIF
   * Egalité Femmes-Hommes
   * Annuaire
   * Programme de mentorat

 * RECHERCHE
   * Algorithmes et structures discrètes
   * Algorithmes et complexité
   * Calcul distribué
   * Combinatoire
   * Théorie et algorithmique des graphes
   * Automates, structures et vérification
   * Automates et applications
   * Modélisation et vérification
   * Preuves, programmes et systèmes
   * Algèbre et calcul
   * Analyse et conception de systèmes
   * Preuves et programmes
   * πr2πr2 (Inria)

 * ÉVÉNEMENTS
   * Evénements de l'IRIF
   * ICALP 2022
   * IRIF Distinguished Talks Series
   * Journées de l'IRIF
   * Rencontres de pôles
   * Séminaires de recherche
   * Algorithmes et complexité
   * Algorithmes et structures discrètes
   * Automates
   * Combinatoire énumérative et analytique
   * Graphes et calcul distribué
   * Preuves, programmes et systèmes
   * Vérification
   * Séminaire des doctorants
   * Séminaires en ligne
   * Graph Transformation Theory and Applications
   * One world numeration seminar
   * Groupes de travail
   * Analyse et conception de systèmes
   * Catégories supérieures, polygraphes et homotopie
   * Logique, automates, algèbre et jeux
   * Programmation
   * Sémantique
   * Théorie des types et réalisabilité
   * Soutenances
   * Soutenances de thèses
   * Soutenances d'habilitation

 * MÉDIATION
   * Fête de la Science
   * Stages scolaires d’observation
   * Exposition 50 ans
   * Projet QuBOBS

 * POINTS CLÉS
   * Prix et distinctions
   * Logiciels
   * Contrats
   * Collaborations internationales
   * L'école thématique EPIT
   * Formation

 * OPPORTUNITÉS
   * Programme visiteurs
   * Soutien à la recherche
   * Enseignant·e·s-chercheurs·euses
   * Chercheurs·euses
   * Postdocs
   * ATER
   * Thèses
   * Stages de master
   * Stages scolaires d’observation

 * INTRANET

 * Traductions de cette page
   * Traductions de cette page
   * Français
   * English

 * Développer/Réduire
 * S'identifier


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), six 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

Proof assistant: A proof assistant is a software tool to mechanize reasoning.
Such a tool typically ensures the well-foundedness of formal definitions, helps
in decomposing a formal proof into intermediate proof goals (i.e., lemmas), and
checks that the reasoning steps are logically consistent.




ACTUALITÉS

27.10.2022
2 papers coauthored by IRIF members will be presented at SODA 2023, January
22-25. Complete list of accepted papers here.



27.10.2022
Gaëtan Douéneau-Tabot, doctorant en 3ème année à l’IRIF, est lauréat 2022 de
deux Best Student Paper Awards remis par les deux principales conférences
organisées par l’EATCS : ICALP et MFCS. En juillet 2022, il a reçu le Best
Student Paper Award track B à ICALP et en août 2022, il a reçu un second prix à
la conférence MFCS. Il nous explique sa recherche dans cette interview écrite.



25.10.2022
Sergio Rajsbaum, a one-year visitor at IRIF, has received the Computer Science
National Prize of Mexico. His research mainly focuses on distributed computing
systems: what can be done as a system? What are the limits?



21.10.2022
The FSMP was present at ICALP 2022 this summer and took the opportunity to meet
the computer scientists Patrick Cousot (New York University), winner of the
EATCS prize, Leslie Ann Goldberg (Oxford University), plenary speaker, Craig
Gentry (IBM Research), Zvika Brakerski (Weizmann Institute of Science) and Vinod
Vaikuntanathany (University of Toronto), winners of the Gödel prize, Gaëtan
Douéneau (PhD student at IRIF), best student paper award, and Geoffroy
Couteau(IRIF), member of the organization of this edition. All the videos
interviews here.



21.10.2022
Les 13 et 14 octobre 2022, l'IRIF et le laboratoire MPQ ont proposé aux classes
de lycée un parcours quantique A la Découverte des Technologies Quantiques
incluant une conférence sur la cryptographie, un atelier sur le protocole BB84,
un atelier sur les ions piégés et un autre sur les photons intriqués.



21.10.2022
Du 7 au 17 octobre 2022, l’IRIF et l’UFR d’Informatique ont accueilli une
dizaine de classes de fin primaire-début collège dans le cadre des activités de
la Fête de la Science. Au programme, un baptême de programmation et plusieurs
îlots de jeux pour s’initier à l’informatique en s’amusant. Plus d’informations
sur notre page dédiée à la Fête de la Science.



21.10.2022
We are very pleased to welcome Sylvain Douteau, Associate professor at
Université Paris Cité. Learn more about his work in this written interview.



24.10.2022
IRIF now has a HAL webpage, an open archive where authors can deposit scholar
documents from all academic fields.



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 octobre 2022, 14 heures, Salle 3052
Pierre Vandenhove Characterizing Omega-Regularity through Finite-Memory
Determinacy of Games on Infinite Graphs


We consider zero-sum games on infinite graphs, with objectives specified as sets
of infinite words over some alphabet of colors. A well-studied class of
objectives is the one of omega-regular objectives, due to its relation to many
natural problems in theoretical computer science. We focus on the strategy
complexity question: given an objective, how much memory does each player
require to play as well as possible? A classical result is that finite-memory
strategies suffice for both players when the objective is omega-regular. We show
a reciprocal of that statement: when both players can play optimally with a
chromatic finite-memory structure (i.e., whose updates can only observe colors)
in all infinite game graphs, then the objective must be omega-regular. This
provides a game-theoretic characterization of omega-regular objectives, and this
characterization can help in obtaining memory bounds and representations for the
objectives as deterministic parity automata. Moreover, a by-product of our
characterization is a new one-to-two-player lift: to show that chromatic
finite-memory structures suffice to play optimally in two-player games on
infinite graphs, it suffices to show it in the simpler case of one-player games
on infinite graphs.

These results are based on joint work with Patricia Bouyer and Mickael Randour
and have been published in the proceedings of STACS 2022.



Analyse et conception de systèmes
Mercredi 2 novembre 2022, 14 heures, Salle 1007
François Pottier (Inria Paris) “You Only Linearize Once”, with elegance

Séminaire des doctorants
Jeudi 3 novembre 2022, 11 heures, 3052
Mouna Safir Non encore annoncé.

Catégories supérieures, polygraphes et homotopie
Vendredi 4 novembre 2022, 14 heures, Salle 1007
Léonard Guetta (Max Planck Institute, Bonn) Les préfaisceaux en groupoïdes comme
modèles des types d'homotopie


Le but de cet exposé est de présenter le résultat suivant : pour toute catégorie
test A, la catégorie des groupoïdes internes à la catégorie des préfaisceaux sur
A modélise les types d'homotopie, et ce de manière “canonique”. Il s'agit donc
d'une généralisation du résultat de Crans-Joyal-Tierney qui traitait le cas
simplicial, lui-même généralisation du résultat célèbre de Kan qui affirme que
la catégorie des groupes simpliciaux modélise les types d'homotopie pointés
connexes, version non-abélienne de l'équivalence de Dold-Kan.

Comme nous le verrons dans l'exposé, l'intérêt principal du résultat précédent
est l'axiomatisation précise de ce qui est entendu par “canonique”, qui
constitue une généralisation de la théorie des catégories tests de Grothendieck.



Graph Transformation Theory and Applications
Vendredi 4 novembre 2022, 15 heures, online
Luciano Baresi (DEIB Politecnico di Milano, Italy) Efficient Dynamic Updates of
Distributed Components Through Version Consistency


Modern component-based distributed software systems are increasingly required to
offer non-stop service and thus their updates must be carried out at runtime.
Different authors have already proposed solutions for the safe management of
dynamic updates. Our contribution aims at improving their efficiency without
compromising safety. We propose a new criterion, called version consistency,
which defines when a dynamic update can be safely and efficiently applied to the
components that execute distributed transactions. Version consistency ensures
that distributed transactions be served as if they were operated on a single
coherent version of the system despite possible concurrent updates. The paper
presents a distributed algorithm for checking version consistency efficiently,
formalizes the proposed approach by means of a graph transformation system, and
verifies its correctness through model checking. The paper also presents CONUP,
a novel prototype framework that supports the approach and offers a viable,
concrete solution for the use of version consistency. Both the approach and
CONUP are evaluated on a significant third-party application. Obtained results
witness the benefits of the proposed solution with respect to both timeliness
and disruption.

Zoom meeting registration link

YouTube live stream



Vérification
Lundi 7 novembre 2022, 11 heures, 1007 and Zoom link
Lorenzo Clemente (University of Warsaw) Zeroness and equality problems for
weighted register automata over equality data


We study the zeroness and equality problems for weighted register automata over
equality data. We reduce these problems to the problem of counting the number of
orbits of runs of the automaton. We show that the resulting orbit-counting
function satisfies a system of bidimensional linear recursive equations with
polynomial coefficients (linrec), which generalises analogous recurrences for
the Stirling numbers of the second kind. We then show that zeroness / equality
of weighted register automata reduces (in exponential time) to the zeroness
problem for linrec sequences.

While such a counting approach is classical and has successfully been applied to
weighted finite automata over finite alphabets and weighted grammars over a
unary alphabet, its application to register automata over infinite alphabets is
novel. We provide an algorithm to decide the zeroness problem for the linrec
sequences arising from orbit-counting functions based on skew polynomials and
variable elimination. This algorithm has elementary complexity.

The complexity can be improved by computing the Hermite normal form of matrices
over a skew polynomial field, which leads to a EXPTIME decision procedure for
the zeroness problem of linrec sequences, and a 2-EXPTIME decision procedure for
the zeroness / equality problems for weighted register automata over equality
data.

These results have appeared in STACS'21 in joint work with Corentin Barloy. It
has been shown in LICS'21 by Bojańczyk, Klin, and Moerman that the complexity of
zeroness / equality of weighted register automata can be improved to EXPTIME,
using novel techniques involving a deep study of orbit-finite vector spaces.



Algorithmes et complexité
Mardi 8 novembre 2022, 11 heures, Salle 2017
Dimitris Achlioptas (University of Athens) The Lovász Local Lemma as Approximate
Dynamic Programming


Imagine facing n switches hooked up to an array of lightbulbs. Each lightbulb is
connected to only a handful of switches and turns on under many, but not all,
configurations of the switches to which it is connected. The satisfiability
question asks whether it is possible to set the switches so that all lightbulbs
are on. Naturally, whenever the answer is positive, flipping a coin for each
switch will cause all lightbulbs to light up with positive probability. At the
heart of the Probabilistic Method is the observation that any multiplicative
underestimation of this probability, no matter how poor, suffices to prove that
the answer is positive. The Lovász Local Lemma (LLL), a cornerstone of the
Probabilistic Method, is a tool for establishing positive probability lower
bounds in the face of conflicting correlations. In this talk, I will present a
new, computational view of the LLL which leads to significant generalizations,
including a passage from the setting of probabilities to that of general
supermodular functions.

One world numeration seminar
Mardi 8 novembre 2022, 14 heures, Online
Wen Wu (South China University of Technology) From the Thue-Morse sequence to
the apwenian sequences


In this talk, we will introduce a class of ±1±1 sequences, called the apwenian
sequences. The Hankel determinants of these ±1±1 sequences share the same
property as the Hankel determinants of the Thue-Morse sequence found by
Allouche, Peyrière, Wen and Wen in 1998. In particular, the Hankel determinants
of apwenian sequences do not vanish. This allows us to discuss the Diophantine
property of the values of their generating functions at 1/b1/b where b≥2b≥2 is
an integer. Moreover, the number of ±1±1 apwenian sequences is given explicitly.
Similar questions are also discussed for 00-11 apwenian sequences. This talk is
based on joint work with Y.-J. Guo and G.-N. Han.

Combinatoire énumérative et analytique
Jeudi 10 novembre 2022, 14 heures, Salle 3052 et zoom
Groupe De Lecture TBD

Preuves, programmes et systèmes
Jeudi 10 novembre 2022, 10 heures 30, Salle 3052
Gabriele Vanoni (Inria Sophia Antipolis) Reasonable Space and the
Lambda-Calculus


The study of computational complexity is based on computational models,
traditionally Turing machines. Space complexity is defined as the maximum number
of cells used during a computation. How could we measure the space complexity of
functional programs? The notion of space is not clear as there is not a fixed
evaluation schema. However, the cost model should be reasonable, i.e. linearly
related with the one of Turing machines. In this talk, I will go through the
journey that led to the definition of the first reasonable space cost model for
the lambda-calculus, accounting for logarithmic space complexity.