Institut de Recherche en Informatique Fondamentale

IRIF Université Paris 7 CNRS L'IRIF est une unité mixe de recherche (UMR 8243) du CNRS et de l'Université Paris-Diderot, issue de la fusion des deux UMR LIAFA et PPS au 1er janvier 2016.

Ses objectifs scientifiques se déclinent selon trois grandes thématiques au cœur de l'informatique : les fondements mathématiques de l’informatique ; les modèles de calcul et de preuves ; la modélisation, les algorithmes et la conception de systèmes.

Poste de maître de conférences

Un poste de maître de conférences est ouvert au concours 2017, affecté à l'IRIF, sur les thématiques de l'unité. Consulter la fiche de poste.

Prochains séminaires

Vendredi 03 mars 2017 · 10h30 · Amphi Turing

Séminaire de l'IRIF · Joost-Pieter Katoen (RWTH Aachen) · IRIF Distinguished Talks Series: Principles of Probabilistic Programming

Probabilistic programming is en vogue. It is used to describe complex Bayesian networks, quantum programs, security protocols and biological systems. Programming languages like C, C#, Java, Prolog, Scala, etc. all have their probabilistic version. Key features are random sampling and means to adjust distributions based on obtained information from measurements and system observations. We show some semantic intricacies, argue that termination is more involved than the halting problem, and discuss recursion and run-time analysis.

Vendredi 03 mars 2017 · 14h30 · Salle 3052

Automates · Guillaume Lagarde (IRIF) · Non-commutative lower bounds

No knowledge in arithmetic complexity will be assumed.

We still don't know an explicit polynomial that requires non-commutative circuits of size at least superpolynomial. However, the context of non commutativity seems to be convenient to get such lower bound because the rigidity of the non-commutativity implies a lot of constraints about the ways to compute. It is in this context that Nisan, in 1991, provides an exponential lower bound against the non commutative Algebraic Branching Programs computing the permanent, the very first one in arithmetic complexity. We show that this result can be naturally seen as a particular case of a theorem about circuits with unique parse tree, and show some extensions to get closer to lower bounds for general NC circuits.

Two joint works: with Guillaume Malod and Sylvain Perifel; with Nutan Limaye and Srikanth Srinivasan.

Vendredi 03 mars 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Maxime Lucas · Structure simpliciale sur les n-branchements et acyclicité de polygraphes

Lundi 06 mars 2017 · 11h00 · Salle 1007

Vérification · Germán Andrés Delbianco (IMDEA Madrid) · Concurrent Data Structures Linked in Time

Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizability and specifying the linearization points of the data structure's procedures. Such arguments are often cumbersome as the linearization points' position in time can be dynamic (depend on the interference, run-time values and events from the past, or even future), non-local (appear in procedures other than the one considered), and whose position in the execution trace may only be determined after the considered procedure has already terminated.

In this talk I will present a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as needed when some appropriate run-time event occurs.

We have named the idea linking-in-time, because it reduces temporal reasoning to spatial reasoning. For example, modifying a temporal position of a linearization point can be modeled similarly to a pointer update in separation logic. Furthermore, the auxiliary state provides a convenient way to concisely express the properties essential for reasoning about clients of such concurrent objects. In order to illustrate our approach, I will illustrate its application to verify (mechanically in Coq) an intricate optimal snapshot algorithm, due to Jayanti.

Mercredi 08 mars 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Pablo Eduardo Rotondo (Automata and applications Group) · TBA