### Institut de Recherche en Informatique Fondamentale

** Research Institute for Foundations of Computer Science **

The scientific objectives of the laboratory are at the core of computer science, focusing on: the mathematical foundations of computer science; computational models and proofs; models, algorithms and system design.

#### Upcoming seminars

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

Vendredi 03 mars 2017 · 14h30 · Salle 3052

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

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

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

#### Events

Vendredi 9 décembre 2016 · 14h · Salle des thèses

Dimanche 15 - Vendredi 20 Janvier 2017 · Jussieu

44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)