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.

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.

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.

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.

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.

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.

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.

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

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

—

Abstract:

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)

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.

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.

* 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.

*

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.

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.

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.

*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.

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.

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.

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.

*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.