Les membres de l'IRIF et les visiteurs sont priés de se conformer aux directives COVID-19 du CNRS et de l'Université de Paris.

L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université de Paris, qui héberge deux équipes-projets 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.

22.5.2020
Jean Krivine (IRIF) discusses how to model an epidemy with Samuel Alizon (MIVEGEC) in a video for Sciences Pop’ Saint-Denis, an association for popular education.

11.5.2020
Thomas Colcombet and Hugo Férée (IRIF) together with Antoine Amarilli and Thomas Schwentick administrate the website for the TCS4F Manifesto, an initiative to reduce the carbon footprint related to Theoretical Computer Science research activities.

11.5.2020

11.5.2020
IRIF PhD student Simon Mauras had a paper accepted at the EC 2020 conference, “Two-Sided Random Matching Markets: Ex-Ante Equivalence of the Deferred Acceptance Procedures”

20.5.2020
Amos Korman (IRIF) has been awarded the 2020 Prize for Innovation in Distributed Computing. The prize will be given during the SIROCCO 2020 conference in July.

(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Tous les évènements sont actuellement organisés à distance.

Vérification
Lundi 8 juin 2020, 11 heures, (online, using BigBlueButton)
Joel Day (Loughborough University) On the structure of solution sets to regular word equations.

For quadratic word equations, there exists an algorithm based on rewriting rules which generates a directed graph describing all solutions to the equation. For regular word equations – those for which each variable occurs at most once on each side of the equation – we investigate the properties of this graph, such as bounds on its diameter, size, and DAG-width, as well as providing some insights into symmetries in its structure. As a consequence, we obtain a combinatorial proof that the problem of deciding whether a regular word equation has a solution is in NP.

Preuves, programmes et systèmes
Mardi 9 juin 2020, 16 heures, Online
Paul Brunet (University College London) Recent developments in concurrent Kleene algebra

Concurrent Kleene algebra (CKA) is an algebraic framework to reason about concurrent programs. In recent years, we have studied several ways of enhancing CKA with extra features, to carry out more sophisticated verification tasks.

In this talk, I will start by recalling the basic definitions of CKA, and its decidability and completeness theorems. We will then take an overview of some of its extensions, considering aspects such as control-flow, memory consistency and mutual exclusion.

This talk is the result of collaborations with Tobias Kappé, Jana Wagemaker, Simon Docherty, Fabio Zanasi, Jurriaan Rot, Alexandra Silva, David Pym, Damien Pous, and Georg Struth.

Algorithmes et complexité
Mardi 9 juin 2020, 14 heures 30, Online
Francesco D'amore (INRIA) On the Search Efficiency of Parallel Lévy Walks in ${\mathbb Z}^2$

Motivated by the Lévy flight foraging hypothesis – the premise that the movement of various animal species searching for food resembles a Lévy walk – we study the hitting time of parallel Lévy walks on the infinite 2-dimensional grid. Lévy walks are characterized by a parameter $\alpha \in(1,+\infty)$, that is the exponent of the power law distribution of the time intervals at which the moving agent randomly changes direction. In the setting we consider, called the ANTS problem (Feinerman et al. PODC 2012), $k$ independent discrete-time Lévy walks start simultaneously at the origin, and we are interested in the time $h_{k,\ell}$ before some walk visits a given target node on the grid, at distance $\ell$ from the origin.

In this setting, we provide a comprehensive analysis of the efficiency of Lévy walks for the complete range of the exponent $\alpha$. For any choice of $\alpha$, we observe that the total work until the target is visited, i.e., the product $k \cdot h_{k,\ell}$, is at least $\Omega(\ell^2)$ with constant probability. Our main result is that the right choice for $\alpha$ to get optimal work varies between $1$ and $3$, as a function of the number $k$ of available agents. For instance, when $k = \tilde \Theta(\ell^{1-\epsilon})$, for some positive constant $\epsilon < 1$, then the unique optimal setting for $\alpha$ lies in the super-diffusive regime $(2,3)$, namely, $\alpha = 2+\epsilon$. Our results should be contrasted with various previous works in the continuous time-space setting showing that the exponent $\alpha = 2$ is optimal for a wide range of related search problems on the plane.

The online reference is here https://hal.archives-ouvertes.fr/hal-02530253

Preuves, programmes et systèmes
Mercredi 10 juin 2020, 15 heures, Online
Yannick Zakowski (University of Penn) Representing recursive and impure programs in Coq: from a toy assembly language to a modular formal semantics for LLVM IR

We will present the design and implementation of _Interaction Trees_ (ITrees), a general-purpose data-structure for representing in Coq potentially divergent, effectful, programs. ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from event handlers, which give meaning to events by defining their semantics as monadic actions. They are expressive enough to represent impure and potentially nonterminating, mutually recursive computations in Coq. Finally, they give rise to a theory enabling equational reasoning, up to weak bisimulation, about ITrees and monadic computations built from them. In contrast to other approaches, ITrees are executable via code extraction.

ITrees are expressive enough to serve as a language of specification for many projects of the DeepSpec ecosystem, making them a convenient Franca Lingua for formal specification, and helping in connecting projects together. Furthermore, their ability to be extracted make them compatible with ambitions of liveness and two-sidedness.

In this talk, we will particularly focus on how ITrees can be used in the context of verified compilation. To this end, we will first introduce the core concepts over a toy language, before sketching how we have been scaling the approach to LLVM IR as part of the Vellvm DeepSpec project.

Preuves, programmes et systèmes
Jeudi 11 juin 2020, 15 heures 30, Online
Claude Stolze Union, intersection and dependent types in an explicitly typed lambda-calculus

We introduce a lambda-calculus decorated with types, enhanced with intersection types, union types, and dependent types. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the “proofs-as-lambda-terms / formulae-as-types” Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. We then discuss the design decisions which have led us to the formulation of these calculi, and provide some examples of applications; and we finally present a software implementation of the Delta-framework, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants.

Séminaire de l'IRIF
Vendredi 12 juin 2020, 10 heures 45, Amphi Turing
[Cancelled] Simon Peyton Jones (Microsoft Research [Cambridge, England]) IRIF Distinguished Talks Series: TBA

Automates
Vendredi 12 juin 2020, 14 heures 30, Online (BigBlueButton)
Kuize Zhang Non encore annoncé.