The calendar of events (iCal format).

Next talks

Special talks
Wednesday February 20, 2019, 1PM, Salle 3052
Giulio Manzonetto (LIPN) A syntactic and semantic analysis of program equivalences

An important problem in theoretical computer science is to determine whether two programs are equivalent. For instance, this is needed to determine whether the optimizations performed by a compiler actually preserve the meaning of the input programs. For lambda calculi, it has become standard to consider two programs as equivalent whenever they can be plugged in any context without noticing any difference in their behavior. Such notion of equivalence depends on the behavior one is interested in observing. We provide syntactic and semantic characterizations of the equivalence arising by taking as observables the beta normal forms, corresponding to completely defined values. As a byproduct we obtain characterizations of the different degrees of extensionality in the theory of Böhm trees.

Special talks
Thursday February 21, 2019, 2PM, Salle 3052
Pablo Arrighi (Aix-Marseille Université) Quantum, automata, computability and universality

After giving a brief introduction to quantum evolutions, whether finite (automata) or infinite-dimensional (operators), I will explore their impact upon computability and universality. Most of the results I will mention rely on a decomposition of quantum operators into quantum automata, which is based upon the tacit assumption of a fixed partial order. Time-allowing, I will try to touch on the topical question of quantum partial orders.

Special talks
Thursday February 21, 2019, 11:45AM, Salle 1007
Samuele Giraudo (Université Paris-Est Marne-la-Vallée) Graded graphs and operads

The set of all integer partitions admits the structure of a graded lattice, called Young lattice, which leads to a beautiful proof for the correspondence between pairs of Young tableaux of the same shape and factorial numbers. All this is due to the fact that this lattice is a differential poset, property introduced by Stanley. A generalization of this property has been provided by Fomin through graded graph duality. Some families of combinatorial objects admit such structures, and the counting of some Hasse walks reveal a nice combinatorics. We present here a new concept of graph duality, pairs of graded graphs of trees, and their lattice properties. We also show how to construct pairs of graded graphs from operads. This allows us to recover existing graphs (like the composition poset or the bracket tree) and to discover new ones.

Special talks
Wednesday Mars 6, 2019, 1PM, Salle 3052
Josef Widder (Technische Universitaet Wien (Vienne, Autriche)) Distributed Algorithms meet Computer-Aided Verification

I will review some of my earlier results on work and time complexity of link-reversal routing algorithms, which were introduced by Gafni and Bertsekas in 1981. The theory we developed for the complexity analysis of these algorithms allowed us also to prove that executions of link reversal algorithms on large graphs are similar (a notion which we make precise) to executions on smaller graphs. The latter result has an interesting application to parameterized model checking of a link-reversal-based resource allocation scheme. In particular, we show cases where verification of large systems can be reduced to checking smaller ones.

The observation that distributed algorithm theory has interesting application in computer-aided verification motivated me to explore this connection in more depth. In the second part of the talk, I will present a line of research that in the recent years led to breakthroughs in parameterized model checking of fault-tolerant broadcasting algorithms. I will close the talk by discussing ongoing research lines and open challenges.

The results on link reversal is joint work with Bernadette Charron-Bost, Matthias Fuegger, Antoine Gaillard, and Jennifer Welch. Parameterized model checking of broadcasting algorithms is joint work with Igor Konnov, Marijana Lazic, and Helmut Veith.

Previous talks

Year 2019

Special talks
Thursday February 7, 2019, 1PM, Salle 3052
Sylvain Schmitz (LSV) The complexity of reachability in vector addition systems

The last few years have seen a surge of decision problems with an astronomical, non primitive-recursive complexity, in logic, verification, and games. While the existence of such uncontrived problems is known since the early 1980s, the field has matured with techniques for proving complexity lower and upper bounds and the definition of suitable complexity classes. This framework has been especially successful for analysing so-called `well-structured systems'—i.e., transition systems endowed with a well-quasi-order, which underly most of these astronomical problems—, but it turns out to be applicable to other decision problems that resisted analysis, including two famous problems: reachability in vector addition systems and bisimilarity of pushdown automata.

In this talk, I will explain how some of these techniques apply to reachability in vector addition systems, a landmark result in theoretical computer science, with applications in an array of fields ranging from program verification to data logics. The decidability of the problem was first shown by Mayr thanks to a decomposition algorithm. I will present succinctly the main ideas behind a tight Ackermannian complexity upper bound obtained with Jérôme Leroux for this algorithm.

Year 2018

Special talks
Thursday September 20, 2018, 10:30AM, Amphi Turing (bâtiment Sophie Germain)
Leonid Libkin (University of Edinburgh) Certain Answers Meet Zero-One Laws

The talk will start with presenting a brief overview of querying incomplete information in databases and the main computational challenges it presents. Querying incomplete data invariably relies on the very coarse classification of query answers into those that are certain and those that are not. Such a classification is often very costly, and we propose to refine it by measuring how close an answer is to certainty.

This measure is defined as the probability that the query is true under a random interpretation of missing information in a database. Since there are infinitely many such interpretations, to pick one at random we adopt the approach used in the study of asymptotic properties and 0-1 laws for logical sentences and define the measure as the limit of a sequence. We show that in the standard model of missing data, the 0-1 law is observed: this limit always exists and can be only 0 or 1 for a very large class of queries. Thus, query answers are either almost certainly true, or almost certainly false, and this classification behaves very well computationally. When databases satisfy constraints, the measure is defined as the conditional probability of the query being true if the constraints are true. This can now be an arbitrary rational number, which is always computable. Another refinement of the notion of certainty views answers with a larger set of interpretations that make them true as better ones. We pinpoint the exact complexity of finding best answers for first-order queries.

Special talks
Thursday July 5, 2018, 2PM, Salle 3052
Laurent Viennot (Inria Paris et IRIF) Introduction to the blockchain

The collaborative construction of a blockchain is the core of Bitcoin protocol for allowing various participants to agree on a list of valid transactions. The talk will be very informal, the intent is to give a very basic introduction on how Bitcoin works and highlight some of the scientific challenges behind it.

Special talks
Tuesday February 20, 2018, 2PM, 3052
Daniela Petrisan (IRIF) Up-To Techniques for Behavioural Metrics via Fibrations

Up-to techniques are a well-known method for accelerating proofs of
behavioural equivalences between systems. In this talk, I 
introduce up-to techniques for behavioural metrics in a coalgebraic
setting and provide general results that show under which conditions
such up-to techniques are sound.
For a system modelled as a coalgebra for a certain functor, the
behavioural distance can be seen as a coinductive predicate using a
suitable lifting of the functor. I will focus on the so called
Wasserstein lifting of a functor for which we provide a new
characterization in a fibrational setting. This is useful for
automatically proving the soundness of up-to techniques via a
generic framework developed in a previous CSL-LICS'14 paper.
I will use  fibrations of predicates and relations valued in a
quantale, for which pseudo-metric spaces are an example. To
illustrate our framework I provide an example on distances between
regular languages.

Special talks
Thursday February 1, 2018, 2PM, 3052
Vincent Danos (ENS) Contractivity of Markov chains (metric couplings)

The module is a continuation of the lecture series by Prakash Panangaden on Labelled Markov Processes, but can be independently followed.

Special talks
Tuesday January 30, 2018, 2PM, 3052
Vincent Danos (ENS) Bayesian inversion​ and approximation

The module is a continuation of the lecture series by Prakash Panangaden on Labelled Markov Processes, but can be independently followed.

Special talks
Thursday January 25, 2018, 2PM, 3052
Prakash Panangaden (McGill University) Quantitative equational logic and free Kantorovich algebras

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”

Special talks
Tuesday January 23, 2018, 2PM, 3052
Prakash Panangaden (McGill University) Metrics for LMPs

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”

Special talks
Thursday January 18, 2018, 2PM, 3052
Prakash Panangaden (McGill University) A dual point of view: LMPs as function transformers

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”

Special talks
Tuesday January 16, 2018, 2PM, 3052
Prakash Panangaden (McGill University) Introduction to LMPs: bisimulation, simulation, logical characterization

Prakash will open his stay with a series of 4 introductory lectures on probabilistic systems: “Introduction to Labelled Markov Processes”