Équipe-projet INRIA $\pi r^2$
Équipe thématique Algorithmes et complexité
Équipe thématique Algèbre et calcul
Équipe thématique Automates et applications
Équipe thématique Combinatoire
Équipe-projet INRIA GANG
Équipe thématique Modélisation et vérification
Équipe thématique Preuves et programmes
Équipe thématique Systèmes complexes, réseaux, calcul distribué
Équipe thématique Théorie et algorithmique des graphes

Jour, heure et lieu

Le mercredi à 11h, salle 3052

Le calendrier des séances (format iCal)


Voir aussi le blog du séminaire, avec des résumés de certains exposés, à l'adresse : https://semidoc.github.io/.

Si vous êtes stagiaire, doctorant extérieur à l'IRIF, ou post-doc, et que vous souhaitez recevoir les annonces du séminaire doctorants, vous pouvez vous inscrire à la liste d'annonce : https://listes.univ-paris-diderot.fr/sympa/subscribe/semidoc-irif

Séances passées

Année 2019

Séminaire des doctorants
Mercredi 6 mars 2019, 11 heures, Salle 3014
Isaac Konan (IRIF) Partitions and Bijections

“For any positive integer n, there are as many partitions of n into distincts parts as partitions of n into odd parts”. This identity stated by Euler is quite trivial to prove by calculations, but not easy show bijectively.

I will discuss bijections for some well-known partition identities, such as Schur partition identity and q-binomial coefficient.

NB: Open talk, all you need is just how to count objects.

Séminaire des doctorants
Mercredi 27 février 2019, 11 heures, Salle 3052
Pierre Ohlmann (IRIF) Lower bounds for arithmetic circuits via the Hankel matrix

We study the complexity of representing polynomials by arithmetic circuits in both the commutative and the non-commutative settings. Our approach goes through a precise understanding of the more restricted setting where multiplication is not associative, meaning that we distinguish (xy)z from x(yz).

Our first and main conceptual result is a characterization result: we show that the size of the smallest circuit computing a given non-associative polynomial is exactly the rank of a matrix constructed from the polynomial and called the Hankel matrix. This result applies to the class of all circuits in both commutative and non-commutative settings, and can be seen as an extension of the seminal result of Nisan giving a similar characterization for non-commutative algebraic branching programs.

The study of the Hankel matrix provides a unifying approach for proving lower bounds for polynomials in the (classical) associative setting. We demonstrate this by giving alternative proofs of recent results proving superpolynomial and exponential lower bounds for different classes of circuits as corollaries of our characterization result.

Our main technical contribution is to provide generic lower bound theorems based on analyzing and decomposing the Hankel matrix. This yields significant improvements on lower bounds for circuits with many parse trees, in both (associative) commutative and non-commutative settings. In particular in the non-commutative setting we obtain a tight result showing superpolynomial lower bounds for any class of circuits which has a small defect in the exponent of the total number of parse trees.

Année 2018

Séminaire des doctorants
Mercredi 28 novembre 2018, 11 heures, Salle 3052
Cédric Ho Thanh (IRIF) Type theoretical approach to opetopes

Opetopes are shapes (akin to globules, cubes, simplices, etc.) introduced to describe laws and coherence in higher categories. Their classical definitions, however, makes them difficult to manipulate efficiently. In this presentation, I will present ongoing works aiming to describe them completely from a type-theoretic standpoint. If time permits, I will showcase a proof checker for opetopes.

Séminaire des doctorants
Mercredi 14 novembre 2018, 11 heures, Salle 3052
Thomas Colcombet (Automata team) Writing (large) LaTeX documents with the knowledge package.

Writing your PhD thesis is a huge work (took me nine months). A burden. Everyone wants it to be THE document that the next generation will read in order to learn the wonderful stuff you have developed at IRIF.

Clearly, there are some pitfalls to avoid. Sometimes a scientifically excellent thesis turns out to be barely usable, because definitions are difficult to find, hard to parse, etc… And the reviewers get mad at you (but say it gently because they are polite). It is your duty to pay attention to all these details (it is also the duty of your PhD advisor to help you in that) and make a document as user friendly as possible.

One can find many documents describing how to write good science/a good thesis on the internet (read some of them!). I will not try to cover this wide subject. My goal in this talk will be to emphasize on some presentation points, and show you how some tools can help you in your writing (this is an advertisement for the LaTeX package « knowledge »).

If you want to test, you can bring your laptop with an up-to-date distribution of LaTeX.

Séminaire des doctorants
Mercredi 31 octobre 2018, 11 heures, Salle 3052
Anupa Sunny & Zhouningxin Wang New PhD session

Explicit, Almost Optimal Epsilon-Biased Sets

by Anupa Sunny

Abstract: This talk is based on a paper by Amnon Ta-Shma on the construction of epsilon biased sets which have a support size close to the Gilbert-Varshamov bound, a notion from coding theory. We will look at the Rozenman-Wigderson construction of the epsilon-biased set in which the bias of a set is amplified by taking a walk over an expander graph. We will then look at Ta-Shma's construction which is based on a modified version of the zigzag product, namely the s-wide replacement product.

Homomorphism of signed graphs

by Zhouningxin Wang

Abstract: The signed graph is a graph whose edges are assigned with the signs + and -. A homomorphism of one graph to the other preserves the adjacencies and incidences of these two edges. We extend the concept of homomorphism for signed graphs. An intuitive example will be given to explain why we consider the homomorphism of signed graphs. We will give the minimum signed graph, namely Spal_5, to which all the signed K_4-minor-free graph admits homomorphism to. In the last part, we will show the necessary and sufficient conditions for a signed K_4-subdivision being a core.

Séminaire des doctorants
Mercredi 17 octobre 2018, 11 heures, Salle 3052
Abishek De & Simon Mauras Newcomers' session

Abishek De : Distributed Control Problem for Free Choice Systems

The distributed synthesis problem is about constructing correct distributed systems, i.e., systems that satisfy a given specification. We consider a slightly more general problem of distributed control, where the goal is to restrict the behavior of a given distributed system in order to satisfy the specification. Our systems are finite state machines that communicate via rendezvous (asynchronous automata). There are a few classes of systems for which the problem has been shown decidable. We solve it for free choice systems, systems whose entire behaviour can be expressed in a (possibly infinite) tree.

Simon Mauras : Social choice theory, and a small survey about rank aggregation

How should we vote? This question has been adressed by philosophers and mathematicians since the XVIIIth century, but no satisfactory solution exists. The talk will start with classical results on social choice theory and move on to the aggregation of rankings seen as an optimization problem. We will discuss NP-Hardness, Hardness of approximation and Approximation algorithms for several variants of this problem.

Séminaire des doctorants
Mercredi 12 septembre 2018, 11 heures, Salle 3052
Farzad Jafarrahmani Denotational semantics of Linear Logic with least and greatest fixpoints

We develop a denotational semantics of full propositional classical linear logic extended with least and greatest fixpoints of formulae (\mu LL) in coherence spaces with totality. The presence of totality predicates, which are a denotational account of the syntactic notion of normalization, allows for dual and non-trivial denotational interpretations of the mu and nu fix point operators involving Knaster Tarski's theorem. We illustrate the construction by means of several examples such as integer numbers system, and by an embedding of Gödel's system T in \mu LL. This specific denotational semantics of muLL is clearly an instance of a more general pattern. We also encode the exponentials of linear logic using least and greatest fixpoints and then explain the difference between the new exponentials and the original ones from denotational semantics point of view. This is based on joint work by Thomas Ehrhard.

Séminaire des doctorants
Mercredi 27 juin 2018, 11 heures, Salle 3052
Victor Lanvin (Équipes Preuves, programmes, et Systèmes) Introduction to gradual typing with union and intersection types

Since the advent of types in programming languages, the two concepts of static typing and dynamic typing have been engaged in a terrible battle. Simply querying “static typing vs dynamic typing” yields more than half a million results on Stack Overflow. On the one hand, static typing provides strong safety guarantees before a program is even executed, by checking during compilation that types are not misused. On the other hand, dynamic typing is more flexible and is better suited to rapid prototyping. With both approaches having strong arguments in their favor, the battle seems endless. Yet, all hope is not lost. Gradual typing is a recent approach that aims at combining the safety guarantees of static typing with the flexibility and development speed of dynamic typing. The idea behind it is to introduce an “unknown” type, used to inform the compiler that additional type checks may need to be performed at run time in some places. Programmers can then “gradually” add type annotations to a program, and control precisely how much checking is done statically versus dynamically. Our work aims at integrating union and intersection types with gradual typing to allow for stronger safety guarantees and a finer control over dynamic types.

Note: this will (should) be a very general presentation about gradual typing and set-theoretic types consisting mostly of practical examples and without too many technical details. Don't hesitate to bring your computer, a book, or your Nintendo Switch™ if you already know the topic. :-)

Séminaire des doctorants
Mercredi 20 juin 2018, 11 heures, Salle 3052
Laurent Feuilloley (Équipes Compsys, GANG et graphes) Distributed decision

In this talk, I will introduce the domain of distributed decision, and review some of the results and insights gathered during my PhD.

The underlying model of this study is the local model. The local model is defined to answer questions of the following type: given a communication network, whose nodes are machines, and edges are communication links, is it possible that the nodes solve some task X, if they communicate only with the nodes that are close to them? A classic problem is colouring: can a node choose a colour, with only the knowledge of a small neighbourhood of the graph, such that the colours chosen by the nodes form a proper colouring of the graph? As in the centralized setting, it is interesting to study decision problems, that are yes-no questions, and to define complexity classes to classify these problems; this is distributed decision.

The complexity class we use as the equivalent of the class P in the centralized setting, is pretty small, and it is then natural to look at some form of non-determinism, to have a chance to understand more problems. In this model, non-determinism can be thought as a piece of global information that can be verified locally. The theoretical motivation is that to understand how local a problem is, one can ask how much global information is needed to solve it. The more practical motivation is that if one can design schemes with little global information then it can help to design more robust distributed algorithms such as self-stabilizing algorithms. The results I will present play with different natural notions of non-determinism, and how they influence the complexity classes defined.

I will spend time to carefully describe the model, thus no prior knowledge is needed.

Séminaire des doctorants
Mercredi 6 juin 2018, 11 heures, Salle 3052
Pierre Ohlmann & Sidi Mohammed Beillahi (Équipe automate & Équipe vérification) Unifying non-commutative arithmetic circuit lower bounds & Robustness of Programs Against Consistency Relaxation

Unifying non-commutative arithmetic circuit lower bounds (Pierre Ohlmann)

We develop an algebraic lower bound technique in the context of non-commutative arithmetic circuits. To this end, we introduce polynomials for which the multiplication is also non-associative, and focus on their circuit complexity. We show a connection with multiplicity tree automata, leading to a general algebraic characterization. We use it to derive meta-theorems for the non-commutative case, and highlight numerous consequences in terms of lower bounds.


Robustness of Programs Against Consistency Relaxation (Sidi Mohammed Beillahi)

Sequential Consistency (SC) and Serializability (Ser) are the classical consistency models for concurrent and distributed programs. They are the intuitive models for developers. Due to the costly synchronization required by the two models, most of existing memory models and distributed implementations of data structures do not use these two models. Instead, in order to reduce the latency and remove unnecessary synchronization, modern processors and databases adopt relaxed and weaker consistency models. However, this weakening of the consistency models implies new unexpected behaviors when running programs over the weaker models. We address in this work the problem of detecting unexpected behaviors of a program that were observed when weakening the consistency model. In particular, we check whether the two sets of executions traces of a program over the SC (resp, Ser) model and some weaker consistency model coincide or not. We characterize the set of executions traces that violate this equality and drive a decision procedure to detect these traces. In the case where there are no traces that violate this equality we refer to a program to be Robust.

A joint work with Ahmed Bouajjani and Constantin Enea

Séminaire des doctorants
Mercredi 23 mai 2018, 11 heures, Salle 3052
Léo Stefanesco (Algebra and calculus, proofs and programs teams) An Asynchronous Soundness Theorem for Concurrent Separation Logic

The talk will start with an introduction to (concurrent) separation logic.


Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this talk, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems [C]S and [C]L which describe the operational behavior of the Code when confronted to its Environment, both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ ⊢ {P}C{Q} defines a winning and asynchronous strategy [π] with respect to both asynchronous semantics [C]S and [C]L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map L : [C]S → [C]L from the stateful semantics [C]S to the stateless semantics [C]L satisfies a basic fibrational property. We advocate that this fibrational property provide a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.

(Joint work with Paul-André Melliès)

Séminaire des doctorants
Mercredi 2 mai 2018, 11 heures, Salle 3052
Emiliano Lancini (Laboratoire d'Informatique de Paris Nord) Box-Total Dual Integrality and k-Edge-Connectivity

In the first half of the 20th century the distribution of electricity became a major issue for many european nations. From this situation arose the problem of building a connected network of minimum length. The mathematical model underlying this problem is the minimum spanning tree problem, it has been investigated by many authors and is now considered a classical problem of combinatorial optimisation.

Nowadays it is often required that telecommunication networks keep unaltered their functionality even after the failure of some of their links. This leads to a generalisation of the minimum spanning tree problem named k-edge-connected spanning subgraph problem.

In this talk we show a characterisation of a graph class in terms of integrality properties of polyhedra naturally associated to the k-edge-connected spanning subgraph problem.

The concept of total dual integrality (TDI) dates back to the works of Edmonds, Giles and Pulleyblank in the late 70's, and is strongly connected to min-max relations in combinatorial optimisation.

The system Ax>=b is TDI if, in the following equation, for each integer vector c, for which the minimum in the following equation is finite, there exists an integer optimal solution for the maximum.

min {cx: Ax>= b} = max {yb: yA = c, y >= 0}

We are interested in the stronger property of box-TDIness. A system Ax>=b is called *box-TDI* if the system Ax >= b, l ⇐ x ⇐ u is TDI for all rational vectors l and u.

We prove that, for k>=2, the k-edge-connected spanning subgraph polyhedron is a box-TDI polyhedron if and only if the graph is series-parallel. Moreover, in this case, we provide a box-TDI system with integer coefficients describing this polyhedron.

Séminaire des doctorants
Mercredi 25 avril 2018, 11 heures, Salle 3052
Raphaëlle Crubillé (Algebra and calculus, proofs and programs teams) Probabilistic Stable Functions on Discrete Cones are Power Series.

The category of probabilistic coherence spaces (PCoh_!), introduced by Danos and Ehrhard, is a fully abstract model for PCF with *discrete* probabilities, where morphisms can be seen as power series. The category Cstab_m, of measurable cones and measurable stable functions, has been introduced by Ehrhard, Pagani and Tasson as a model for PCF with *continuous* probabilities. In this talk, we will study the shape of stable functions when they are between *discrete* cones, and it will allow us to see that PCoh_! is a full subcategory of Cstab_m.

Séminaire des doctorants
Mercredi 18 avril 2018, 11 heures, Salle 3052
Paulina Cecchi & Antoine Allioux (Automata, Combinatorics teams & Algebra and calculus, proofs and programs teams) New PhD student introduction session

* Paulina Cecchi

Title: Some interactions between words combinatorics and symbolic dynamics.

Abstract: Word combinatorics has been fruitfully used to study several topological and mesure-theoretic properties of dynamical systems, through the analysis of suitably chosen symbolic dynamical systems. In this talk, we will introduce some notions of symbolic dynamics and present some examples which illustrate how word combinatorics can be used as a tool to solve questions arising from this branch of mathematics.


* Antoine Allioux

Title: The curse of Martin-Löf identity type

Abstract: The identity type of Intuitionistic Type Theory (ITT) endows types with a structure of infinity-groupoid. This higher structure follows from the fact that the Uniqueness of Identity Proof (UIP) is not derivable in ITT. Homotopy Type Theory (HoTT) takes advantage of this observation by enriching ITT with new principles which are coherent with this interpretation, namely the Univalence Axiom and the Higher Inductive Types (HITs).

HITs are a generalization of inductive types which allow, in addition to create regular inhabitants of an inductive type, to postulate identities between them as well as identities between these identities, and that ad infinitum. It is then tempting to try to present mathematical structures using these new types like one would do in mathematics using generators and relations.

However, problems quickly arise as soon as one needs a strict equality. Indeed, the identity type expresses a weak equality leading to the usual coherence problems. Trying to solve these naively, we run into the problem of having to define an infinite sequence of coherence data.

If HoTT is to be a credible foundation of mathematics, the question of formalizing structures which need a strict equality is crucial. The answer to this question rests, in part, upon our achievement to either present these structures differently in the existing theory or to enrich it so that it becomes tractable to express them.


Séminaire des doctorants
Mercredi 11 avril 2018, 11 heures, Salle 3052
Brieuc Guinard Intermittent Locomotion in Graphs

Everyone who has ever lost their keys in a busy room knows that they cannot move at full speed and hope to find them ; one must slow down enough as not to miss them. This compromise between speed of moving and success of detection is not specific to humans, of course, and in fact is commonly encountered in foraging animals, and even in cell biology. This opposition between relocation and detection can even lead to an intermittent behavior, i.e. with different phases during the search. We model such search processes by memoryless explorations on graphs, i.e. random walks, where you can decide at each step to query a node or not. The goal is to balance the time spent walking and the time spent querying.

Séminaire des doctorants
Mercredi 28 mars 2018, 11 heures, Salle 3052
Yann Hamdaoui (Proofs and Programs and Conception and Analysis of Systems teams) Translating a Concurrent Lambda Calculus into Linear Logic proof (nets)

Logical translations of intuitionnistic logic into linear logic have been studied for their sole interest. Incidentally, they provide translations of simply typed lambda calculus to linear logic: apart from its theoretical insights, the asynchronous nature of linear logic's cut-elimination make it also an interesting target of compilation, enabling distributed and/or parallel execution models. We present here translation of a richer typed calculus, featuring parallel threads and references, into a fragment of linear logic.

Séminaire des doctorants
Mercredi 21 mars 2018, 11 heures, Salle 3052
Mengchuan Zou (Theory and algorithmics of graphs team) Generalization of binary search in trees and other structures

The tree search problem is the following generalization of the binary search problem. A search strategy is required to locate an unknown target node t in a given tree T. Upon querying a node v of the tree, the strategy receives as a reply an indication of the connected component of T \ {v} containing the target t. The cost of querying each node is given by a known non-negative weight function, and the considered objective is to minimize the total query cost for a worst-case choice of the target.

We will also introduce some known facts on other structures and how tree search problem is related to other problems via equivalences.

Séminaire des doctorants
Mercredi 21 février 2018, 11 heures, Salle 3052
Zeinab Galal & Ranadeep Biswas (Algebra and computation & Modeling and verification) Species of structure: a Bridge between Differential Lambda Calculus and Combinatorics & Verifying Database Histories

*Species of structure: a Bridge between Differential Lambda Calculus and Combinatorics*

Species of structure lie at the intersection of combinatorics and denotational semantics. They were first introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics and multiple tools were developed for the resolution of differential equations of species in this setting. Later, Fiore presented a generalized definition that both encompasses Joyal's species and constitutes a model of linear logic.

We will first introduce and connect the different viewpoints of species of structure and their series counterpart (analytic and normal functors) presented by Joyal, Girard and Hasegawa. Next, we will examine how the bicategory of generalized species of structure forms a model of differential linear logic.

As our end goal is to develop methods of resolution of differential equations for λ-terms, we will investigate the possible directions to tackle this problem.


*Verifying Database Histories*

Popular databases offer control over the isolation level to which the operations in one transaction are visible to the operations in other concurrent transactions. Lower levels allow weaker consistency. So, we have to ensure that the histories of a database are consistent with their isolation levels.

Unfortunately, these isolation levels are mostly defined as low-level operations which makes it complicated to reason about the behavior of the system running under those isolations.

In this talk, we will present some popular isolation levels and consistency criteria for databases. We will introduce a framework, in which it becomes easier to formally reason about the behavior of a system. Then we will explore the complexities of deciding some consistency criteria using that framework.

Séminaire des doctorants
Mercredi 14 février 2018, 11 heures, Salle 3052
Narcisse Nya Kamtchoum (LIP6) Modèles analytiques pour les performances des réseaux cellulaires

Afin d'augmenter le débit et accroître la couverture réseau, les réseaux mobiles ne cessent d'évoluer rapidement vers des technologies caractérisées par des interfaces radio plus sophistiquées. Par exemple, alors que le déploiement des réseaux 4G ne faisait que commencer, les premières mises à jour des solutions LTE-A étaient déjà planifiées par les opérateurs et Actuellement, les technologies 5G font l'objet de recherches actives dans le monde entier. Ces changements rapides sont motivés par l'explosion du trafic mobile, tel que prédit par de nombreuses études et observé dans les réseaux actuels.

Cependant, les opérateurs ont du mal à s'adapter à la proportion toujours grandissante d'utilisateurs mobiles et à leur offrir une qualité d'expérience (QoE) satisfaisante. Dans ce contexte, il est importante pour les opérateurs et les équipementiers de disposer d'outils simples et efficaces pour mieux comprendre le comportement de leurs réseaux et évaluer la qualité des services offerts aux utilisateurs. Notre objectif est de proposer des modèles analytiques pour l'évaluation des performances des réseaux cellulaires en tenant compte de la mobilité des utilisateurs. Tout en permettant de résoudre des problèmes d'évaluation de performance les plus complexes, ces modèles se doivent d'être simple afin de faciliter leur utilisation.

Séminaire des doctorants
Mercredi 7 février 2018, 11 heures, Salle 3052
Nicolas Jeannerod (Team Analysis and conception of systems) Unix filesystems and First-Order Theory of an Algebra of Feature Trees with Updates

In the CoLiS project (for Correctness of Linux Scripts), our mid-term goal is to automatically verify certain properties on installation packages that may include shell scripts. In order to do that, we want to write a symbolic execution tool that would compute abstract specification for each installation script in term of filesystem transformations.

We investigate a logic of an algebra of trees with an update operation, which expresses that a tree is obtained from an input tree by replacing a particular direct subtree while leaving the rest intact. This operation improves on the expressivity of existing logics of tree algebras in our case of feature trees. These allow for an unbounded number of children of a node in a tree.

We show an efficient way of testing the satisfiability of existential clauses in this algebra that can lead to an efficient implementation of our symbolic execution engine. We also show the decidability of the first-order theory of this algebra via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers.

Séminaire des doctorants
Mercredi 31 janvier 2018, 11 heures, Salle 3052
Thomas Williams (Gallium, INRIA) Refactoring ML programs using ornaments

Ornaments are a way to describe changes in datatype definitions that preserve their recursive structure, reorganizing, adding, or dropping some pieces of data. The relation between two types given by an ornament can be used to define a lifting relation between functions operating on a bare definition and functions operating on the ornamented structures. Thus, ornaments provide a way to specify the desired behaviour of a program refactored to work on an ornamented datatype.

In this talk, I will explain how ornaments can be used to automatically lift a function. I will present a prototype implementation of lifting along ornaments for a subset of OCaml and describe some families of use cases. I will introduce a principled approach to obtaining a lifting from the base code, as abstraction followed by specialization. I will explain how this approach allows us to prove the correctness of the lifting.

Séminaire des doctorants
Mercredi 24 janvier 2018, 11 heures, Salle 3052
Alessandro Luongo & Ny Aina Andriambolamalala (Algorithms and complexity team & Combinatorics team) Recent updates in quantum machine learning & Election de leader dans un réseau radio simple saut avec detection de collision

*Recent updates in quantum machine learning*

In this talk we are going through some recent algorithms in the field of quantum machine learning. Most of the techniques use tools from quantum algorithmics such as counting, optimizing, estimating distances and singular values which will be introduced here. Using these primitives it's possible to build more complex operations of a matrix algebra. I'll also describe a classical machine learning algoritm in the process of being translated in a fully fledged quantum algorithm. This is the first biologically plausible quantum algorithm with an exponential speedup w.r.t the dimension of the space and the number of datapoints. This quantum algorithm has been simulated and used to classify handwritten digits with high accuracy.

*Election de leader dans un réseau radio simple saut avec detection de collision*

Les résultats de Dan Willard (1986) montrent un algorithme randomizé d'élection de leader en temps moyen $O(\log\log{n})$.

Depuis, la question de savoir s'il existe un algorithme convergeant en temps log-logarithmique mais avec très forte probabilité est ouverte.

Nous répondons affirmativement à cette question. Nous montrons aussi comment utiliser nos résultats pour élaborer des protocoles d'élection dans divers modèles de systèmes distribués.

Année 2017

Séminaire des doctorants
Mercredi 20 décembre 2017, 11 heures, Salle 3052
Leo Stefanesco (Équipes “Preuves et Programmes” et “Algèbre et Calcul”) “A concise introduction to logical relations” followed by “A Logical Relation for Monadic Encapsulation of State”

1st part (E for Everyone): A concise introduction to logical relations

Logical relations are a powerful technique to prove properties about programs. In particular, for proving that two programs are contextually equivalent.

In this talk, we will see that, in System F (aka the polymorphic lambda calculus), the only program of type ∀ a, a → a is the identity.

I will also sketch how to extend logical relations to realistic languages such as ML.

2nd part (POPL talk rehearsal):

A Logical Relation for Monadic Encapsulation of State

We present a logical relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our logical relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such relational results have been proven for a language with monadic encapsulation of state. We have formalized all the technical development and results in Coq.

Séminaire des doctorants
Mercredi 13 décembre 2017, 11 heures, Salle 3052
Simon Halfon (ENS Cachan) Well Quasi-Orders and Extreme Stratospheric-Complexity-Classes of Death — Beaux pré-ordres et classes de complexité stratosphériques de la mort

It is widely known how to prove the termination of an algorithm using well-founded orderings. It is however usually believed that no complexity upper bound can be derived from these termination proof, often seen as non-constructive. In this talk, I will present some ideas to infer upper bounds from such termination proofs. I will try to give you a taste of the complicated combinatorics behind, that results in surprisingly high complexities. Oxygen bottles and pressure suits required, we are going beyond Elementary.

No special knowledge is required to follow the talk.

Nous savons tous qu’il est très pratique pour prouver la terminaison d’un algorithme d’utiliser des ordres bien fondés. Cependant, il est commun de penser que cette technique ne donne aucune information sur la complexité de l’algorithme, car la preuve est non constructive. Dans cet exposé, je présenterai quelques idées pour extraire une borne supérieur de complexité d’une telle preuve de terminaison. J’essaierai de vous donner une idée de la combinatoire compliquée que cela engendre, et qui résulte en des complexité très élevée. Bouteilles d’oxygène et combinaisons pressurisées obligatoire, on s’envole au delà de l’Élémentaire.

Aucune connaissance spécifique n'est nécessaire pour suivre l'exposé.

Séminaire des doctorants
Mercredi 6 décembre 2017, 11 heures, Salle 3052
Axel Osmond & Yassine Hamoudi 1)

1) 1) “Algebra and calculus” and “proofs and programs” teams, (2) Algorithms and complexity team.) New PhD student introduction session. (1) From pointless topology to formal topology (2) ACC0 and multiparty communication: fighting the log n barrier.
(1) While point-set topology is highly practical as a framework to dospatial reasoning, one can rise some ontological and logical suspicionsabout naive notion of points as they constitute idealized objects withsomewhat inaccessible aspects in a constructive and finite point ofview. Locales and Frames theories are two deeply entangled realms aimedat rebuilding topology on latticial and categorical foundations, inwhich usual notions of points, opens, subspaces, separability,compacity… can be reexpressed as first order algebraic properties inlatticial context, or both generalized and made constructive.Formal topology goes further into this last direction, using systems ofaxioms about coverings as a deductive systems which leads to atype-theoretic flavored, predicative and constructive topology, endowedwith multiple and finer notions of points, separability… and suitedfor intuitionistic reasoning. (2) The Number On the Forehead model is a multiparty communication game between k players that collaboratively want to evaluate a given function F : X1 x … x Xk → Y on some input (x1, …, xk) by broadcasting bits according to a predetermined protocol. The input is distributed between the players in such a way that each player i sees all of it except xi (as if xi is written on the forehead of player i).A central open question in this model, called the log n barrier, is to find a function which is hard to compute when the number of players is polylog(n) or more (where the xi's have size poly(n)). This has an important application in circuit complexity, as it could help to separate ACC0 from other complexity classes.In this talk, we will recall first the connection between ACC0 and communication complexity, and then describe a new efficient communication protocol that prevents some important functions from breaking the log n barrier.
Séminaire des doctorants
Mercredi 22 novembre 2017, 11 heures, Salle 3052
Jules Chouquet (Proofs and Programs team) Linear logic proof nets and Taylor expansion.
I will first introduce linear logic proof nets, for the multiplicative and exponential fragment (MELL), and I will especially insist on the computational meaning of the exponential boxes: these are constructions containing the possibility of duplication and deletion of entire parts of the structures (all the non linear part of the calculus).Once these notions are introduced, I will explain how it is possible to express this computational paradigm in a linear setting through a syntactical Taylor expansion. The idea is to understand exponential boxes in a differential variant of linear logic, and to represent it with linear combination.If we have time, I will try to give an idea of some algebraic issues concerning this construction, and a method to show for example, that the normal form of the Taylor expansion of a MELL always converges.NB: Taylor expansion is here analogical to the lambda calculus (with its differential version too) one, if someone heard about it, it can give a first intuition.
Séminaire des doctorants
Mercredi 15 novembre 2017, 11 heures, Salle 3052
Chaitanya Leena Subramaniam (“Algebra and calculus” and “proofs and programs” teams) Homotopy type theory and the fibred structure of dependent types
This is another session of the PhD introduction series.Chaitanya will do a 30 minutes talk. Given that the talk will not last as long as usual, we will also take advantage of the opportunity to discuss the organization of the seminar.Abstract:The talk will not be about my particular research problem. It will seek insteadto give a gentle pictorial introduction to the inherent structure of dependent types and how this structure determines what dependent types anddependently-typed programs (or proofs) *mean*.The focus will be on why this structure naturally leads to homotopy type theoryand univalence. As a bonus, and if time permits, there will be some remarkson univalence and extensionality.
Séminaire des doctorants
Mercredi 8 novembre 2017, 11 heures, Salle 3052
Francesco Antonio Genco (Technische Universität Wien) Typing Parallelism and Communication through Hypersequents
We present a Curry–Howard correspondence for Gödel logic based on a simple natural deduction reformulating the hypersequent calculus for this logic. The resulting system extends simply typed λ-calculus by a symmetric higher-order communication mechanism between parallel processes. The normalization proof employs reductions that implement forms of code mobility. We consider this result from a broader perspective and, following A. Avron's 1991 thesis on the connection between hypersequents and parallelism, we discuss the generalisation of the employed techniques for other intermediate logics.
Séminaire des doctorants
Mercredi 25 octobre 2017, 11 heures, Salle 3052
Cédric Ho Thanh & Isaac Konan (Algebra and calculus team / Combinatorics team) New PhD student introduction session
This special session will introduce two new PhD students who will each be giving a short talk.Isaac Konan, Bijective proof and generalization of Siladic's theoremIn a recent paper, Dousse introduced a refinement of Siladic̀’s theorem on partitions, by using the method of weighted words, where the different parts could take 2 colours. The proof of that refined theorem used some recursive equations with q-series. In this presentation, I will give the big lines of a bijective proof of the Dousse’s theorem, moreover which could be extended on a coloring with more than 2 colours.Cédric Ho Thanh, Opétopes, Réécriture, et KoszulitéMa thèse consiste en 3 mots que je vais tenter d'expliquer.
Séminaire des doctorants
Mercredi 11 octobre 2017, 11 heures, Salle 3052
Hadrien Batmalle (Équipe Preuves et Programmes) From Cohen's Forcing to Classical Realisability: A New Approach
English abstract belowDu forcing à la réalisabilité classique: une nouvelle approcheLa réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calculs (lambda-calcul avec continuations, domaines…). L'intérêt est double: côté informatique, il s'agit d'extraire des interprétations calculatoires de preuves classiques; côté mathématique, on obtient de nouveaux modèles de ces théories classiques (les deux aspects étant intimement liés). Une grande partie de la recherche en réalisabilité classique étudie la structure de ces modèles, qui apparaissent comme une généralisation du forcing de Cohen. Nous nous intéresserons ici à une nouvelle méthode pour exporter des propriétés des modèles de forcing aux modèles de réalisabilité, qui permet de construire des interprétations de deux théories contradictoires dans un même modèle de calcul, ce qui ouvre la voie à une analyse fine des conséquences calculatoires de la présence ou non de tel ou tel axiome.From Cohen's Forcing to Classical Realisability: A New ApproachClassical realisability is a framework for interpreting classical theories in mathematics, such as the ZF set theory, in various models of computation (lambda-calculus with continuations, domains…). The goal is twofold: from the computer scientist's point of view, this is a method for extracting computational interpretations out of classical proofs; from the mathematician's, this is a trove of new models for these classical theories (both sides being tightly interwoven). A good deal of the research in this area is focussing on the structure of these models, arising as a generalisation of Cohen's forcing. In this talk we'll present some consequences of a new method for exporting properties of Cohen's forcing models into properties of classical realisability models. In particular we obtain interpretations of two incompatible theories in the same model of computation, which clears the path to studying the computational consequences of the presence, or lack thereof, of some axiom.
Séminaire des doctorants
Mercredi 27 septembre 2017, 11 heures, Salle 3052
Baptiste Louf & Victor Lanvin (Combinatorics and PPS teams) New PhD student introduction session
This special session will introduce two new PhD students who will each be giving a short talk. Here are the titles and abstracts of the talks:Combinatorial maps : algebraic and bijective enumerationCombinatorial maps (which are embeddings of graphs on surfaces) are wellstudied objects in combinatorics, which have applications in otherdomains, such as quantum gravity. The goal is to enumerate them(sometimes exactly, sometimes asymptotically). For this purpose, one canresort to (among other things) bijective or algebraic methods. Thealgebraic method is often more powerful and yields results more easily,however bijections give a more in-depth understanding of the models.Often, formulas are found via powerful methods, then people try tore-prove them bijectively. In this talk, I present what I’m focusing on,on the bijective side (Carell-Chappy formula) and on the algebraic side(KP equations). If time permits, I will explain a simple bijection Idiscovered during my Master’s internship.Gradual Set-Theoretic TypesA static type system can be an extremely powerful tool for a programmer, providing early error detection, and offering strong compile-time guarantees onthe behavior of a program. However, compared to dynamic typing, static typingoften comes at the expense of development speed and flexibility, as statically-typed code might be more difficult to adapt to changing requirements. Gradualtyping is a recent and promising approach that tries to get the best of bothworlds, by allowing the programmer to finely tune the distribution of dynamic and static checking over a program.However, this “gradualization” is sometimes too coarse, and an expression isoften either fully dynamic or fully static. We argue that adding full-fledged unionand intersection types (a.k.a. set-theoretic types) to a gradual type systemsolves this issue by making the transition between dynamic typing and static typing smoother.
Séminaire des doctorants
Mercredi 28 juin 2017, 11 heures, Salle 3052
Tommaso Petrucciani (PPS team) Semantic subtyping: an introduction
Many type systems for programming languages include a notion of subtyping. Subtyping is often defined syntactically by a formal system, but this gets increasingly complex when union, intersection, and negation types are introduced.In the semantic subtyping approach, instead, types are interpreted as sets and subtyping is defined in terms of set containment. Then, an algorithm is derived from the definition. While the algorithm is complex, the interpretation of types serves as a fairly simple specification. This approach also ensures that union and intersection on types behave as the corresponding operations on sets.I will give an introduction to this approach and show how to define subtyping semantically for types including arrows, union, intersection, and negation, following [Frisch et al., 2008]. Then, we will look at ongoing work on adapting this approach (originally studied for call-by-value languages) to lazy semantics.[Frisch et al., 2008] A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping, JACM, 2008.
Séminaire des doctorants
Mercredi 14 juin 2017, 11 heures, Salle 3052
Timo Zijlstra & Emmanuel Arrighi Quantum algorithms and Learning With Errors- based Cryptography & Distance Labels and Tree Skeletons
Quantum algorithms and Learning With Errors- based Cryptography:Post quantum cryptography is meant to replace today's standards like RSA and Elliptic Curve Cryptography (ECC), since these standards are threathened by quantum algorithms. The most researched post-quantum candidates are based on lattice problems, and in particular the Learning with Errors (LWE) problem. It is assumed that there exists no quantum algorithm that solves this problem efficiently. However, in a particular setting and under some strong hypothesis, it is very easy to solve LWE using a generalization of the Bernstein-Vazirani quantum algorithm. We will take a look at possible quantum cryptanalysis on LWE-based cryptographic applications. Distance Labels and Tree Skeletons: To answer distance queries on a fix known graph, it is interesting to doprecalculation in order to reduce query time. A methode is to use HubLabeling. Hub Labeling works well on road transport network. We willtake a look at this methode and introduce the notion of SkeletonDimension which give an insight on why it works well on road network.
Séminaire des doctorants
Mercredi 31 mai 2017, 11 heures, Salle 3052
Clément Jacq (PPS team) A playful introduction to game semantics (category-light)
(English abstract below)Une introduction ludique à la sémantique des jeux (allégée en catégories)La sémantique des jeux est une branche de la théorie des modèles dont l'objectif est d'interpréter des formules de certaines logiques sous forme de jeux à deux joueurs. Son objectif initial était de lier les notions de vérité et de validité à des concepts de théorie des jeux tels que l'existence de stratégies gagnantes…Après quelques exemples historiques, nous nous intéresserons dans cet exposé de manière informelle à un cas plus récent ou la sémantique des jeux modélise désormais des langages de programmation.En guise de conclusion, nous évoquerons l'aspect formel avec la notion de structure catégorielle.
A playful introduction to game semantics (category-light)Game semantics is a branch of model theory that aims at interpreting formulas of a given logic as two-player games. Initially, it was developed to link the notions of truth and validity to game-theoretic notions such as the existence of winning strategies.After an historical example, we will look informally at a more recent case of game semantics where the games are used to model programming languages. At the end, we'll mention the formal part with the notion of categorical model.
Séminaire des doctorants
Mercredi 17 mai 2017, 11 heures, Salle 3052
Pierre Vial (PPS team) An Introduction to Intersection Type Systems, and a New Answer to Klop's Problem
Although the following abstract is (mostly) in French, the talk will be in English if there are non-French speakers in the room.L'exposé aura deux buts:1) Présenter les systèmes de types-intersection (ITS, intersection typesystems), en particulier, les ITS à intersection non-idempotente.Je commencerai par des rappels basiques en lambda-calcul. On verra enquoi la représentation des lambda-termes par des arbres (bienqu'élémentaire) permet de comprendre la façon dont les ITS sont conçuset vérifient naturellement des propriétés que les systèmes de typessimples ne peuvent (raisonnablement) pas avoir. Par exemple, dans unITS, un terme est normalisable (i.e. il termine) ssi il est typable. Paropposition, dans un système de types simples, on aura seulementl'implication “Si le terme t est typable, alors il est normalisable”(*Propriété de Terminaison*). La notion de normalisation (i.e.terminaison) admet de nombreuses variantes: on en verra deux, laréduction de tête (HN, Head Normalization) et la réduction faible (WN,Weak Normalization). On verra aussi que les ITS ont des conséquences enlambda-calcul qui sont *externes* à la théorie des types.Etant donné un système de type Sys (que Sys soit un ITS ou un système detypes simples, d'ordre supérieur ou non), la propriété de terminaison(typable dans Sys ⇒ normalisable) est souvent difficile à établir (ondoit généralement recourir à un argument dit de réalisabilité, attribuéà Tait). Cependant, je présenterai le système R, introduit par Gardneret de de Carvalho, dans lequel l'opérateur d'intersection peut être vucomme non-idempotent et la terminaison repose sur un argument trèssimple que nous verrons ensemble.2) Présenter un article (accepté récemment à LICS) traitant delambda-calcul et de réduction infinitaires et dont voici l'abstract:Infinitary Intersection Types as Sequences: a New Answer to Klop’s ProblemWe provide a type-theoretical characterization of weakly-normalizingterms in an infinitary lambda-calculus. We adapt for this purpose thestandard quantitative (with non-idempotent intersections) typeassignment system of the lambda-calculus to our infinite calculus.Our work provides a positive answer to a semi-open question known asKlop’s Problem, namely, finding out if there is a type systemcharacterizing the set of hereditary head-normalizing (HHN)lambda-terms. Tatsuta showed in 2007 that HHN could not be characterizedby a finite type system. We prove that an infinitary type system endowedwith a validity condition called approximability can achieve it.As it turns out, approximability cannot be expressed when intersectionis represented by means of multisets. Multisets are then replacedcoinductively by sequences of types indexed by integers, thus defining atype system called System S.
Séminaire des doctorants
Mercredi 3 mai 2017, 11 heures, Salle 3052
Alexandre Nolin (Algorithms and complexity Group) Quantum, a look through nonlocality
In this talk I will try to give an introduction to the mathematical framework of quantum computing, completely disconnected of the underlying theory of quantum physics. After an exposition of a circuit model for quantum computing, we will split those circuits into two parts (the infamous Alice and Bob) and talk about the behaviours of those bipartite systems, more specifically somewhat counter-intuitive phenomenons like entanglement and nonlocality. Finally, we will see how those phenomenons are relevant in the study of communication complexity, and discuss recent results.
Séminaire des doctorants
Mercredi 19 avril 2017, 11 heures, Salle 3052
Pierre Cagne (PPS team) Lawvere’s hyperdoctrines and notions of equality
This talk will present hyperdoctrines, a widget invented by Lawvere in the late 70’s to give a categorical account of type theories. It has the advantage to dissociate every construction/rules of a type theory: structural rules, logical rules, quantifier rules, equality rules, etc. As a welcomed side effect, it questions the legitimacy of such rules. In particular, we will take some time to study the equality and the relevance of its usual definition, and try to give a feeling of Lawvere’s seminal thoughts on HoTT. If time permits, we shall discuss the insight of such an approach about a (for now non well established) “directed type theory”, by which is roughly meant a type theory in which paths between terms are not necessarily reversible.
Séminaire des doctorants
Mercredi 5 avril 2017, 11 heures, Salle 3052
Guillaume Lagarde (Automata and applications Group) On the stability of the Lempel-Ziv compression algorithm
LZ78 is a very simple lossless data compression algorithm published by Abraham Lempel and Jacob Ziv in 1978. It is fair enough to expect a certain stability from a data compression algorithm against small perturbation on the input. In this direction, Jack Lutz among with others asked the following question, so-called “the one-bit catastrophe”: given an infinite word w, can the compression ratio of w be different from 1w? In this presentation, I will give some results in this fashion; in particular I would like to give the intuition of the fact that a catastrophe can indeed occur in LZ78.Joint work with Sylvain Perifel.The presentation will just use basic combinatorics.
Séminaire des doctorants
Mercredi 22 mars 2017, 11 heures, Salle 3052
Gabriel Radanne (PPS team) GADTs gone mild
Generalized Algebraic Data Types, often also called “Poor man'sdependent types”, are an extension of regular sum and product types thatis available in OCaml and Haskell.Since their adoption in “mainstream” languages, GADTs have been knownfor allowing to elegantly write toy typed interpreter at the cost ofhorrible type error messages and numerous headaches. Or, as Yaron Miskysaid, “I assumed that it was the kind of nonsense you get when you letcompiler writers design your programming language.”.In this talk, I will present GADTs, what they are, and what usefulthings we can do with them. This will take us on quite a journey, withsome traces of C, a pinch of memory layout, a cameo from pushdownautomata and a healthy amount of Prolog. The only requirements will be apassing familiarity with OCaml and the caffeinated beverage of your choice.
Séminaire des doctorants
Mercredi 8 mars 2017, 11 heures, Salle 3052
Pablo Eduardo Rotondo (Automata and applications Group) Continued Fractions and the Recurrence of Sturmian Words
In this talk I will present various aspects of Continued Fractions, motivating and explaining their relation to the factors of the so-called Sturmian Words. We conclude by a probabilistic study of the recurrence function of Sturmian Words, which is common work with Brigitte Vallée (CNRS, Univ. Caen).
Séminaire des doctorants
Mercredi 22 février 2017, 11 heures, Salle 3052
Lucas Boczkowski (Algorithms and complexity Group) Minimizing Message Size in Stochastic Communication Patterns: Fast Self-Stabilizing Protocols with 3 bits
The talk is based on a paper whose abstract is the following:This paper considers the basic PULL model of communication, in whichin each round, each agent extracts information from few randomly chosenagents. We seek to identify the smallest amount of information revealedin each interaction (message size) that nevertheless allows forefficient and robust computations of fundamental informationdissemination tasks. We focus on the Majority Bit Disseminationproblem that considers a population of n agents, with a designatedsubset of source agents. Each source agent holds an input bit and eachagent holds an output bit. The goal is to let all agents convergetheir output bits on the most frequent input bit of the sources (themajority bit). Note that the particular case of a single source agentcorresponds to the classical problem of Broadcast (also termed RumorSpreading). We concentrate on the severe fault-tolerant context ofself-stabilization, in which a correct configuration must be reachedeventually, despite all agents starting the execution with arbitraryinitial states. In particular, the specification of who is a source andwhat is its initial input bit may be set by an adversary.We first design a general compiler which can essentially transform anyself-stabilizing algorithm with a certain property (called “thebitwise-independence property”) that uses l-bits messages to onethat uses only (log l)-bits messages, while paying only a smallpenalty in the running time. By applying this compiler recursively wethen obtain a self-stabilizing Clock Synchronization protocol, inwhich agents synchronize their clocks modulo some given integer T,within O(log n log T) rounds w.h.p., and using messagesthat contain 3 bits only. We then employ the new Clock Synchronizationtool to obtain a self-stabilizing majority broadcast protocol whichconverges in O(log n) time, w.h.p., on every initialconfiguration, provided that the ratio of sources supporting theminority opinion is bounded away from half. Moreover, this protocol alsouses only 3 bits per interaction.Based on joint work with A. Korman and E. Natale.
Séminaire des doctorants
Mercredi 25 janvier 2017, 11 heures, Salle 3052
Thibaut Girka (PPS team) Oracle-based Differential Operational Semantics (or Explaining program differences with programs)
We present a formal framework to characterize differences betweendeterministic programs in terms of their small-step semantics. Thislanguage-agnostic framework defines the notion of /difference languages/ inwhich /oracles/—programs that relate small-step executions of pairs of programswritten in a same language—can be written, reasonned about and composed.We illustrate this framework by instantiating it on a toy imperativelanguage and by presenting several /difference languages/ ranging from trivialequivalence-preserving syntactic transformations to characterized semanticdifferences. Through those examples, we will present the basis of ourframework, show how to use it to relate syntactic changes with their effect onsemantics, how one can abstract away from the small-step semanticspresentation, and discuss the composability of oracles.
Séminaire des doctorants
Mercredi 11 janvier 2017, 11 heures, Salle 3052
Fabian Reiter (Automata and applications Group) Asynchronous Distributed Automata
The goal of this talk is to raise interest in the connections betweendistributed computing and formal logic. I will illustrate thisrelatively unexplored area of research by presenting an equivalenceresult between two very specific systems. The distributed computingside will be represented by a network of identical finite-statemachines that communicate in an asynchronous manner, while the formallogic side will be represented by a small fragment of least fixpointlogic (more specifically, a fragment of the modal mu-calculus).