Séminaire

Équipe thématique Algorithmes et complexité
Équipe thématique Algèbre et calcul
Équipe thématique Automates et applications
Équipe thématique Combinatoire
Équipe thématique Modélisation et vérification
Équipe-projet Inria Picube (Inria)
Équipe thématique Preuves et programmes
Équipe thématique Théorie et algorithmique des graphes


Jour, heure et lieu

Le jeudi à 16h, salle 3052

Le calendrier des séances (format iCal).
Pour ajouter le calendrier des séances à votre agenda favori, souscrire au calendrier en indiquant ce lien.


Contact(s)

Bienvenue à une nouvelle série de séminaires hebdomadaires pour les membres non permanents, le jeudi à 16 heures, salle 3052. Il s'agit d'une excellente occasion pour tous les membres non permanents, y compris les postdocs, les ATER, les doctorants et les stagiaires, de se rencontrer, de partager leurs intérêts de recherche et de créer une atmosphère scientifique accueillante.

Prochaines présentations

Toutes les présentations sont ouvertes à tous, quel que soit le niveau d'expérience. Nous encourageons les débutants à y assister et à apprendre de nos collègues plus expérimentés.

Rafraîchissements

Pour rendre le séminaire encore plus agréable, nous aurons le gâteau de l'IRIF juste après le séminaire !

Nous nous réjouissons de vous y voir !

Forum de questions-réponses

Si vous souhaitez poser ou répondre à une question d'informatique lors du séminaire, vous pouvez utiliser ce lien.


Séminaire des membres non-permanents
Jeudi 16 janvier 2025, 16 heures, Salle 3052
Umberto Tarantino Non encore annoncé.

Séminaire des membres non-permanents
Jeudi 23 janvier 2025, 16 heures, Salle 3052
Miriam Marzaioli Non encore annoncé.

Séminaire des membres non-permanents
Jeudi 30 janvier 2025, 16 heures, Salle 3052
Vincent Moreau Non encore annoncé.

Séminaire des membres non-permanents
Jeudi 6 février 2025, 16 heures, Salle 3052
Emile Larroque Non encore annoncé.

Séminaire des membres non-permanents
Jeudi 13 février 2025, 16 heures, Salle 3052
Adrienne Lancelot AG des membres non-permanents
À confirmer.



Année 2024

Séminaire des membres non-permanents
Jeudi 5 décembre 2024, 16 heures, Salle 3052
Carmen Arana (PhD Student) How graph theorists use topology

In 1955 Kneser conjectured that the k sized subsets of the numbers from 1 to n can be partitioned into n-2k+2 classes such that each class contains only disjoint elements, but that it cannot be partitioned this way into n-2k+1 classes. This conjecture can be nicely expressed as a graph coloring problem. Twenty years later, in order to solve this problem, Lovasz introduced the topological method in graph theory, and more largely combinatorics. In this talk, we will explain what this method entails, and explain how it is used on the example of this theorem.

Séminaire des membres non-permanents
Jeudi 21 novembre 2024, 16 heures, Salle 3052
Manu Catz (PhD Student) Polygraphs and Oriented Shapes

The most accessible way to visualize a (small) category is to consider its objects as vertices and its morphisms as oriented edges, forming some sort of graph. Polygraphs extend this intuition to form higher categories, where higher cells can be seen as oriented faces between edges, oriented solids between faces, &c. I will illustrate this construction with two families of categories, the oriented simplices and the oriented cubes, as well as showcase two operations that relate them when seen as constructed by a parametric language.

References:

Polygraphs: Dimitri Ara et al. Polygraphs: From Rewriting to Higher Categories.

Orientals: Ross Street. “The algebra of oriented simplexes” ; Dimitri Ara, Yves Lafont, and François Métayer. Orientals as free algebras.

Oriented Cubes: Iain R. Aitchison. The geometry of oriented cubes.

Parametricity: Hugo Herbelin and Ramkumar Ramachandra. A parametricity-based formalization of semi-simplicial and semi- cubical sets.

Séminaire des membres non-permanents
Jeudi 24 octobre 2024, 16 heures, Room 3052
Avinandan Das (PhD Student) Fooling around with Graphs : Forcing Alice and Bob to make mistakes to prove communication lower bounds.

We are in the 2-party communication setup which is as follows. There are two players Alice and Bob who are given as inputs, graphs G_1 and G_2 respectively. They communicate with each other to compute some function f on the graph G_1 \cup G_2. How many bits of communication are required between them in order for them to compute the function f ? In this technique, we will first set up the communication model, consider graph problems like maximum matching, degeneracy and coloring in this model and then delve into the technique of fooling sets in order to arrive to communication bandwidth lower bounds for these problems in the two party set-up. Fooling set is a mechanism to design inputs for Alice and Bob such that if too few bits are communicated between them, then both of them are ``fooled'' into making mistakes. If time permits, we will also peek into the mechanism of proving lower bounds for problems in streaming model using communication lower bounds.

Séminaire des membres non-permanents
Jeudi 17 octobre 2024, 16 heures, Room 3052
Niklas Kochdumper (Post-Doc) Automated Verification of Dynamic Systems

Reachability analysis is a powerful technique that can be used to verify that dynamic systems, such as autonomous cars, robots, or power grids, are robustly safe despite disturbances, measurement errors, and uncertain behavior of other agents in the environment. However, one substantial bottleneck of all state-of-the-art reachability algorithms is the necessity to adequately tune specific algorithm parameters, such as the time step size, which requires expert knowledge. This talk presents a new type of reachability algorithm, which already tunes all parameters internally until safety of the system with respect to unsafe sets or temporal logic specifications can either be proven or falsified. Our automated algorithm enables also non-experts to apply reachability analysis with ease, and we hope that this will facilitate a more widespread use of formal methods for dynamic systems in both research and industry in the future.

Séminaire des membres non-permanents
Jeudi 10 octobre 2024, 16 heures, Salle 3052
Everyone Introductory session & social event

We will start a new series of non-permanent weekly seminars with an introduction section, during which everyone can briefly share their name, background, and research topic (if desired). This is a casual and friendly setting, so don't be shy!

After the session, we will have some refreshment and play some games, everyone is welcome.

Séminaire des membres non-permanents
Jeudi 20 juin 2024, 16 heures, Salle 1020
Jean Abou Samra Parsing: from theory to practice and back

As Russ Cox put it, “Historically, regular expressions are one of computer science's shining examples of how using good theory leads to good programs. Today, regular expressions have also become a shining example of how ignoring good theory leads to bad programs.” In this talk, I will first review the classical theory of parsing: context-free grammars, pushdown automata, regular expressions, efficient algorithms such as LL(k), LR(k), LALR and Thompson. Next, I will describe several extensions of these tools devised by practitioners, among which PEG grammars, and extended regular expressions. The complexity consequences of these extensions have led to entire classes of software vulnerabilities such as regular expression denial of service (ReDOS), which exploits extended regular expressions of high matching complexity. I will explain how this gives rise to interesting theoretical questions, such as “Can we decide if an extended regular expression is vulnerable?”, and conclude with a state of the art of current research on this topic. There are no prerequisites.

Séminaire des membres non-permanents
Jeudi 13 juin 2024, 16 heures, Salle 3052 and Zoom Link
Arjan Cornelissen Algorithms for volume estimation of convex bodies

Estimating the volume of a convex body is a canonical problem in theoretical computer science. Its study has led to major advances in randomized algorithms, Markov chain theory, and computational geometry. In particular, determining the query complexity of volume estimation has been a longstanding open question. Most of the previous work focuses on the high-dimension limit. In this work, we tightly characterize the (deterministic, randomized and quantum) query complexity of this problem in the high-precision limit, i.e., when the dimension is constant.

Séminaire des membres non-permanents
Jeudi 6 juin 2024, 16 heures, Salle 3052
Allen Ibiapina k-Linkage on Temporal Graphs

Given a graph \( G \) and a set of \( k \) pairs of vertices, the \( k \)-Linkage Problem asks whether there exists a set of \( k \) paths such that each path connects a given pair of vertices, and each vertex in the graph is used by at most one of these paths. When one consider temporal graphs, where the graph's structure can change over time, the \( k \)-Linkage Problem takes on new variations. This seminar focuses on a specific version where we seek time-respecting paths that connect the given pairs of vertices, ensuring that at any given time, each vertex is occupied by at most one path. I will present results on the parameterized complexity of this problem when \( k \) is given as a parameter.

Séminaire des membres non-permanents
Jeudi 30 mai 2024, 16 heures, Salle 3052 and Zoom Link
Victor Arrial The Bang-Calculus: An Accessible Introduction to Subsuming Paradigms

The lambda calculus is a formal system that serves as the foundation for functional programming languages. It supports different evaluation strategies, resembling the evaluation processes of various programming languages such as Haskell and OCaml. The Bang Calculus is an extension of the lambda calculus introduced to provide explicit counterparts for these strategies, thus allowing a uniform study of them.

In this talk, we will present the Bang Calculus and provide multiple examples of (simple) properties that can be subsumed within this framework. Absolutely no prerequisites are required.

Séminaire des membres non-permanents
Jeudi 23 mai 2024, 16 heures, Salle 3052 and Zoom Link
Dung Bui Efficient MPC from correlated randomness

Secure multiparty computation (MPC) is an area of
cryptography that creates methods for parties to jointly compute a
function over their inputs while keeping those inputs private. MPC
often is constructed from a trusted source of correlated randomness to
achieve better efficiency.

In this talk, we show how useful forms of correlated randomness can be
generated using a cheap, one-time interaction, followed by only
“silent” local computation. This is achieved via a pseudorandom
correlation generator (PCG), a deterministic function that stretches
short correlated seeds into long instances of a target correlation.
However, PCGs come with a major limitation: The expansion of the
correlated seeds is an “all-or-nothing” procedure, where the target
correlation is produced all at once without enabling fast random
access to the long output. Later, a pseudorandom correlation function
(PCF) is introduced to overcome these limits by designing short
correlations of keys that can be expanded “on the fly” to a virtually
unbounded number of pseudorandom correlation instances, and which
further enable fast random access to these instances.

This talk is very general and intuitive, no cryptography background is
required.

Séminaire des membres non-permanents
Jeudi 16 mai 2024, 16 heures, Salle 3052 and Zoom link
Clément Ducros How to Achieve Secure Computation Using Coding Theory?

Secure Multiparty Computation (MPC) aims at enabling different parties to compute functions based on private inputs. Providing the parties with additional correlated and random inputs enables highly efficient MPC protocols. But how do we construct this additional correlated randomness? In this presentation, I will discuss the construction of pseudorandom correlation generators (PCG), focusing on the special case of two-party random oblivious linear evaluations (OLEs). We will explore the foundational concepts introduced by Boyle et al. (2020), examine their limitations, and demonstrate how coding theory significantly contributes to the security analysis and efficiency of the construction. This presentation is based on collaborative work with Maxime Bombar, Dung Bui, Geoffroy Couteau, Alain Couvreur, and Sacha Servan-Schreiber.

Séminaire des membres non-permanents
Jeudi 2 mai 2024, 16 heures, Salle 3052 and Zoom link
Ulysse Lechine Introduction to Kolmogorov complexity

In 1963 Andrey Kolmogorov came up with the definition of Kolmogorov complexity : the kolmogorov complexity of a string $w\in {0;1}^*$ noted $K(w)$ is the size of the smallest program $p$ which stops after printing $w$. In this sense it can for instance be made formal to say that 0101010101010101 is a less random/complex string than 56748195473159418. This notion of complexity is universal and robust (for instance it doesn't matter in which language the program $p$ is written), it has been studied for its own sake and is also used in number theory, combinatorics, probabilisic theory, computability theory, complexity theory (P=NP) etc… where it has led to new or simplified proofs.

We will present an introduction to Kolmogorov theory and some beautiful applications. We will also talk about a new recent result of Léchine and Seiller ( https://hal.science/hal-04539439 ) which features a very neat open combinatorics problem which you may help solve. No background is needed.

Séminaire des membres non-permanents
Jeudi 25 avril 2024, 16 heures, Salle 3052
Etienne Objois A width-independent algorithm for approximating the $\ell_p$ norm of a nonnegative matrix and its applications.

Given a matrix $A$ with $m$ rows and $n$ columns, we want to approximate the maximum value of $||A x||_p$ when $||x||_q <= 1$. For general matrices, a $(1-\epsilon)$ approximation of the problem is hard, but for nonnegative matrices, when $q >= p >= 1$, the problem can be transformed into a concave maximization problem. In this talk, we will present a width-independent (i.e., the running time dependence on $n m$ is at most poly-logarithmic) algorithm to find $(1-\epsilon$) approximations in time nearly $O(nnz/\epsilon)$.

In the second part of the talk, we will see how such an algorithm can be used to compute competitive oblivious linear routings.

Séminaire des membres non-permanents
Jeudi 28 mars 2024, 16 heures, Salle 3052 and Zoom link
Arturo De Faveri A gentle introduction to universal algebra

Universal algebra concerns the study of those mathematical objects that behave like 'algebraic structures' (i.e. groups, rings, vector spaces…). This talk is divided into two parts. In the first we try to understand what 'algebraic structures' have in common, offering an overview of the basic concepts of universal algebra. In the second we survey some selected topics that link universal algebra with logic and computer science.

Séminaire des membres non-permanents
Jeudi 21 mars 2024, 16 heures, Salle 3052
Olivier Idir Explorable automata : expressiveness and decidability

Explorable automata lie on the border between deterministic and non-deterministic automata: they are non-deterministic automata where it is possible to solve the non-determinism. When given a word spelled one letter at a time, an automaton is said explorable if there exists a way to produce an accepting run by moving forward tokens in a given number of copies of the automata. (the case with exactly one copy corresponds to the history-deterministic case). In this joint work with Denis Kuperberg, I studied explorable automata on infinite words. More specifically, I studied, for different accepting conditions, their expressiveness and the decidability of the explorability property.

Séminaire des membres non-permanents
Jeudi 14 mars 2024, 16 heures, Salle 3052 and Zoom link
Klara Nosan How we compute with polynomials

We all learned the formula for solving quadratic equations in school, but how would you go about finding the roots if you are given a polynomial of, say, degree 10? How about if someone asked you to give an algorithm to do that? The latter is an example of the type of problems considered in algorithmic algebra. In this talk, I will try to give a high level overview of computational problems concerning polynomials and systems of polynomials. We will look at different representations of polynomials and talk about problems such as polynomial identity testing or determining whether a system of equations admits a common solution. No (algebraic or other) preliminaries required — I will even remind you of the quadratic formula in case you forgot it.

Séminaire des membres non-permanents
Jeudi 7 mars 2024, 16 heures, Salle 3052 and Zoom link
Christoph Egger Proving Negative Results: Oracle Separations

We're all used to and familiar with proving interesting results and of course sometimes we can also prove that theorems are wrong. But is there something substantial one can say about the absence of proofs? The more philosophically inclined can go back to Gödel's famous work and convince themselves that there will always be true statements that are not provable in any particular system.

As such a statement will necessarily depend on a concrete theory of proof we are going to look into a specific technique commonly used in complexity theory called oracle separations (Impagliazzo, Rudich, STOC 1989) and how we can use an elementary counting argument to create a contradiction to proofs (Gennaro, Trevisan, FOCS 2000).

Given the topic at hand we are going to struggle with too many negations. Also it comes natural to re-introduce reduction proofs but it clearly helps to have seen those already (say in undergrad np completeness). There's virtually no cryptography in it and I assume we can keep it broadly accessible to all lab members even though it is a somewhat technical topic!

Séminaire des membres non-permanents
Jeudi 29 février 2024, 16 heures, Salle 3052
Huan Zhou Graph colouring: Extending brooks’ Theorem

In graph theory, graph colouring is a special case of graph labelling; it is an assignment of labels traditionally called ‘’colours’’ to elements of a graph subject to certain constraints. In its simplest form, it is a way of colouring the vertices of a graph such that no two adjacent vertices are of the same colour, which is called vertex colouring. The problem of colouring a graph arises in many practical areas such as sports scheduling, designing seating plans, exam timetabling, the scheduling of taxis and so on.

In this talk, I will introduce some basic conceptions and theorems of graph colouring, such as brooks’ Theorem. Moreover, I will introduce a new conception called k-truncated-degree choosability and some open problems.

Séminaire des membres non-permanents
Jeudi 15 février 2024, 16 heures, Salle 3052
Aymeric Walch What is the meaning of functional random programs ?

Random programs are very useful. In particular, they allow to write programs that are very efficient on average (such as randomized quick sort). It is however a bit hard to define what these programs compute without some form of hand waving. The goal of semantics is to define the probability distributions associated to a random program in a systemic and a modular way.

This approach has received an increase in interest following the rise of probabilistic programming. The goal of probabilistic programming is to write a random program, called a model, and to provide generic inference tools to condition this program with regard to some observations. It is then very important to assign a precise meaning to the distribution computed by the model, and to the inferred distribution. This is where semantics shines.

The goal of this talk is to provide an intuition of what the semantics of a functional programming language with higher order should look like. Surprisingly, this is deeply tied to linear logic and differential linear logic. In particular, a probabilistic program should be interpreted as an “analytic maps” in some sense.

Please be reassured. We will not talk about categorical abstract nonsense. The goal of the talk is to stay as grounded as possible and to provide intuitions, not to explain why the Kleisli category of the exponential comonad of probabilistic coherence spaces is a cartesian closed category (it is, though).

This will be a whiteboard talk.

Séminaire des membres non-permanents
Jeudi 8 février 2024, 16 heures, Salle 3052 and Zoom link
Loïc Peyrot Polymorphic records for dynamic languages

An argument in favour of dynamically-typed programming languages is their flexibility, enabling quick code writing and prototyping. But this is also a weakness, as many bugs are only detected when executing the program. Hence, statically-typed versions of well-known languages are in rapid expansion, such as Typescript or Luau. To guarantee the safety of a program without sacrifing expressivity, augmenting types with set operations, such as union and intersection, has proven very useful. Considering those set-theoretic operators naturally leads to so-called semantic subtyping: types are interpreted as sets, union and intersection types with the corresponding set operators, and subtyping is derived from set inclusion in the interpretation. Systems with semantic subtyping and set-theoretic types now support first-order polymorphism à la ML, a powerful programming abstraction. This kind of polymorphism however, is not sufficient when considering a language with extensible records (or structs), as it does not capture precise enough typings. In this talk, I will give an introduction to type systems with set-theoretic types and semantic subtyping. I will showcase some programs with typing failures, and show how the addition of row polymorphism for records solves the problem. I will then describe how we integrated row polymorphism to a type system with set-theoretic types, semantic subtyping and first-order polymorphism.

Séminaire des membres non-permanents
Jeudi 1 février 2024, 16 heures, Salle 3052 and Zoom link
Roman Edenhofer Quantum Space-bounded Computation and Graph Connectivity

Recent advances on linear algebraic problems such as matrix inversion suggest that quantum computers are strictly more powerful with limited space than classical computers. Building on these results we discuss a possible quantum advantage for graph connectivity. That is the problem of deciding whether two nodes in a graph are connected and is of fundamental importance to space-bounded complexity theory. The talk will cover some aspects of spectral graph theory and unambiguous computation. No quantum background is required to follow it.

Séminaire des membres non-permanents
Jeudi 25 janvier 2024, 16 heures, Salle 3052 and Zoom link
Rida Ait-El-Manssour Synthesising Simple loop Programs and Toric Ideals

Automatic generation of loop invariants is a fundamental challenge in software verification. A simpler version of this challenging task is the polynomial invariants generation for loops with linear updates. In the first part of the talk, I will explain for a given loop how to construct all its polynomial invariants and the relationship to Toric ideals. In the second part, I will reverse the problem from invariant synthesis to loop synthesis. That is, given an algebraic property we ask to construct a loop with an infinite set of reachable states that has the given property as an invariant. This is based on ongoing project with George Kenison, Mahsa Shirmohammadi, and Anton Varonka.

Séminaire des membres non-permanents
Jeudi 18 janvier 2024, 16 heures, Salle 3052 and Zoom link
Shamisa Nematollahi Airports and Railways Problem

In the problem of airports and railways (AR), the goal is to establish an efficient transportation network for a given set of cities with minimum cost. This involves the strategic placement of airports in select cities and the establishment of railway connections between each city without airport to an airport. Once implemented, this network will enable passengers to travel from their hometowns to any desired destination by utilizing a combination of flights and trains. As a formal definition, we are given a complete graph G = (V,E) with weightsontheverticesa:V →R+,lengthoftheedgesl:V ×V →R+,anda positive integer k as the capacity parameter. The goal is to compute a spanning forest R of G and a subset A ⊆ V of minimum cost such that each component in R has one open facility and the number of cities in each component is at most k (the capacity constraint). The cost of the solution (A, R) is measured as \sum_{v∈A} a(v) + \sum_{e∈E(R)} l(e). In the unsplittable demand version of the problem (ARUD), additionally, we are given a function b : V → R+ that defines a non-zero demand for each city and the goal is to find a network of trees with minimum cost such that the total demand in each component is at most k. In this talk, we’ll discuss different versions of the problem (when the problem defined on different networks), bi-factor approximation algorithms for the metric AR and ARUD problems which violates the capacity constraints by O(k), and some complexity results of the problem.

Séminaire des membres non-permanents
Jeudi 11 janvier 2024, 16 heures, Salle 3052
Srinidhi Nagendra Two directions to testing distributed systems using coverage: random and reinforcement learning

Distributed systems have been a crucial component in the growth of large scale databases that power most of modern internet. While the algorithms used to run these systems are proven to be sound, the gap between implementations and on-paper algorithms leaves room for errors. Recurring downtimes in popular services such as Facebook and Cloudflare are mainly due to bugs in these implementations. In this talk, I will present two new approaches to test these implementations to guarantee correctness. One, improves on well known techniques for fuzzing using a TLA specification. Two, uses intelligent Reinforcement learning techniques to cover edge cases more efficiently and find new bugs. This is on going work with researchers from MPI and TU Delft.


Année 2023

Séminaire des membres non-permanents
Vendredi 15 décembre 2023, 11 heures, Salle 3052 and Zoom link
Vincent Moreau Stone spaces explained and exemplified

Stone spaces appear at the interface of computer science, logic and general mathematics. In this talk, we will give a gentle introduction to Stone spaces, distilling a few key examples that illustrate their peculiarities in an accessible way. We will also be hinting towards Stone duality and other related topics, such as applications in automata theory. No prerequisites.

Séminaire des membres non-permanents
Jeudi 7 décembre 2023, 16 heures, Salle 3052
Esaie Bauer Proof theory in Multiplicative-Additive Linear Logic

In this presentation, I will provide an introduction to proof theory within the context of non-wellfounded proof systems. A non-wellfounded proof is generated by finitely branching logical rules, but potentially resulting in an infinitely deep proof tree. After defining the system, I will present a proof of cut-elimination for the $\mu$-MALL system, drawing from the work of Baelde et al. in 2016. Furthermore, I will discuss how we aim to extend this result with Alexis Saurin.

Séminaire des membres non-permanents
Jeudi 30 novembre 2023, 16 heures, Salle 1007 and Zoom Link
Mariana Milicich Useful Evaluation, Inductively and Quantitatively

In this talk, I'll present the first inductive characterization of the useful evaluation for open call-by-value, with its results. We achieve such characterization by parameterizing the evaluation relation with the information provided by the context in which the computation takes place. Then, we study some of its properties, and compare it with other evaluation strategy. Lastly, we propose a quantitative type system (with tight rules) for the strategy.

Séminaire des membres non-permanents
Jeudi 23 novembre 2023, 16 heures, Salle 3052
Herman Goulet-Ouellet Density of rational languages

I will present ongoing work about densities of regular languages under invariant measures of minimal shift spaces, which will serve as a pretext for an introduction to symbolic dynamics, with some algebra and ergodic theory thrown in the mix.

Séminaire des membres non-permanents
Jeudi 16 novembre 2023, 16 heures, Salle 3052 and Zoom link
Sacha Servan-Schreiber The power of subtractive secret sharing in secure computation

Two-party computation occasionally enables more efficient protocols compared to even three party computation. Two important building blocks enabling efficient two-party protocols are (1) distributed point functions (DPFs) and homomorphic secret sharing (HSS). In this talk, we will examine what properties enables these building blocks and why they are primarily restricted to the two party setting. This will provide insights into why multi-party computation protocols are more difficult to design and what assumptions allow us to circumvent these barriers.

Séminaire des membres non-permanents
Jeudi 9 novembre 2023, 16 heures, Salle 1007
Minh-Hang Nguyen Agreement tasks: An introduction of Combinatorial Topology in Distributed Network Computing

Agreement tasks, e.g. consensus, k-set agreement, have been intensively studied in distributed computing for the last 30 years. A natural question is to find better lower bounds on the number of rounds for algorithms solving agreement tasks. In this talk, I will first define Local and Know-all models, agreement tasks, and some basic notions in combinatorial topology. Then, I will give an example to see a relation between the solvability of consensus and the path connectivity of a protocol complex. Finally, I will present some useful tools for lower bounds on the round complexity of agreement tasks.

No prior knowledge is required.

Séminaire des membres non-permanents
Jeudi 26 octobre 2023, 16 heures, Salle 3052 and Zoom link
All Non-Permanent Members Assemblée Générale

This will be a discussion in order to prepare the HCERES meeting. A group of 6 or 7 non permanents members should be constituted, they will meet for 30 minutes with the HCERES comitee the Wednesday 29th of November.

Séminaire des membres non-permanents
Jeudi 19 octobre 2023, 16 heures, Salle 1007
All Non-Permanent Members Introductory session

This will be an introductory session where we invite all (new and old!) non-permanent members to come and talk about their research interests. Each talk should be 2-5 minutes long, and understandable by everyone.

Séminaire des membres non-permanents
Jeudi 12 octobre 2023, 16 heures, Salle 3052
Lucie Guillou How to verify Parameterised Broadcast Networks?

In a broadcast network, a node sends a message to all of its neighbors in a synchronous fashion. The communication topology is represented as a graph and each node executes a finite-state automaton. A problem of interest in verification is to determine if such a network allows for a node to reach an error state of the automaton, this is what we will call the coverability problem. When the communication topology is given, this problem is decidable, however, when it is not the case, one needs to check that for all possible communication topologies, an error state is never reached, and the problem becomes undecidable. It is the parameterised version of the coverability problem for broadcast networks, note that neither the number of nodes nor the graph is fixed. I will present this model as well as the undecidability proof before talking about a new restriction on the network aiming to regain decidability. As far as I know (this is some ongoing work), this restriction allows in some very particular cases to regain restrictions but fails in most cases.

This talk will not assume any prior knowledge in verification nor in distributed networks.

Séminaire des membres non-permanents
Jeudi 28 septembre 2023, 16 heures, Salle 3052
Emily Clement Layered controller synthesis for dynamic multi-agent systems

We present a layered approach to solve a multi-agent control problem. This methods mixes three domains: timed automata, SMT and reinforcement learning, in order to obtain the best of each: the method based on timed automata solves the combinatorial aspect of the problem, the SMT refine our model into a more realistic one and the two methods are combined into a SWA-SMT solver. Finally, the Reinforcment Learning trains the policy in order to show that the initial dataset generated with the the SWA-SMT solver is crucial for the overall success of the method.

Séminaire des membres non-permanents
Jeudi 22 juin 2023, 16 heures, Olympe de Gouges 147 and Zoom link
Anna Gujgiczer (Budapest University of Technology and Economics) Introduction to Information Theoretic Graph Parameters

This talk is going to be an introduction to some information theoretic graph parameters. Perhaps the most famous of these is the Shannon capacity which can be described as follows. Over a communication channel the sender can send some characters and on the other side some pairs of these characters are distinguishable to the receiver, but some pairs of them are confusable with positive probability. We can construct a graph of this channel: the vertices are the characters, and two of them are connected by an edge if they are distinguishable. If we want zero-error in the communication, then the maximum number of distinguishable messages of length 1 is just the clique number of this graph, and the maximum number of longer messages of fixed length is the clique number of some power of this graph. The Shannon capacity is defined as the limit of the normalized values of these clique numbers, and is the theoretical upper bound on the efficiency of zero-error communication over a discrete, memoryless channel. Some other parameters, such as the Sperner capacity or the Witsenhausen rate, can be defined in a similar way and are also of information theoretic relevance. We will discuss these parameters and their relation with other known graph invariants.

The talk is introductory, so we will go through a few examples and skip the difficult proofs. No previous knowledge in information theory is required.

Séminaire des membres non-permanents
Jeudi 15 juin 2023, 16 heures, Olympe de Gouges 147 and Zoom link
Maud Szusterman (IMJ-PRG) How non-negative matrices and fooling sets / randomised protocols can help bounding the extension complexity

Affine constraints can describe a polytope P : the minimal number of inequalities required for a description is called the size of the polytope (it is its number of facets). For the sake of linear optimization, affine extensions Q of P can be useful : by adding a few extra variables, one can sometimes exponentially decrease the complexity (i.e. the size) of the description. This area has motivated research both in search of lower and upper bounds on the extension complexity (minimal size of an affine extension Q) of polytopes. Equivalent definitions (via non-negative rank, and via randomised communication protocols) of extension complexity xc(P) have been found (Yannakakis, Faenza-Fiorini), we will review them and some upper or lower bounds which use this alternative characterization.

NB : no previous knowledge in polytopes or in complexity theory is required.

Séminaire des membres non-permanents
Jeudi 8 juin 2023, 16 heures, Olympe de Gouges 147 and Zoom link
Bernardo Jacobo-Inclan Timed automata and information of timed languages

Timed automata, as their name suggests, are a kind of automata in which time is taken into account. This is done by the presence of a number of clocks which can be tested or reset. Ever since they were introduced by Rajeev Alur and David L. Dill, they have been very important for modelling real-time systems. This presentation will give an introduction to the topic of timed automata, as well as present some usual tools and concepts for analysing them. Among these is the notion of clock regions, which spawn a very visual way of understanding the behaviour of these automata, and which will allow to state Puri's result characterizing reachability for a path.

Time permitting, I will talk about how starting from these tools, with some necessary additional work, it was possible to establish a characterization of the amount of “information per time unit” generated by a given automaton. This notion of “information” is to be defined during the presentation, it is the one we introduced recently, inspired by Kolmogorov and Tikhomirov's notion of epsilon-entropy.

Séminaire des membres non-permanents
Jeudi 1 juin 2023, 16 heures, Olympe de Gouges 147 and Zoom link
Thomas Colcombet Some guides for writing your thesis, or some other documents

At some point in our lives, one has to write comprehensive (and long) scientific documents, like a PhD or an habilitation thesis, for instance, or simply a long paper. When on the other side, as a reader or as a reviewer, one has to decipher these documents. Indeed, we discover in them clever ideas, marvellous algorithms, wonderful theorems. But also, one sometimes gets (very) angry and frustrated by the manuscript, because it is written in a way that makes the life hard for the reader.

In this talk, I will try to give some hints that may be of help in such writing processes. I will also talk of some technical tools that may turn to be useful, and in particular the « knowledge package » for LaTeX (that I happened to have written).

Séminaire des membres non-permanents
Jeudi 25 mai 2023, 16 heures, Olympe de Gouges 147 and Zoom link
Sophie Laplante Qubobs: interactive devices to explain quantum computing

We introduce interactive devices and a visual representation of qubits to assist in explaining quantum computing to a broad audience. In this talk we will briefly explain the representation then we will invite the audience to play with games designed to develop intuition on quantum states, entanglement, and quantum circuits. This is the first time we will be testing out our games and we welcome feedback on the experience from audience members.

This is joint work with Loris Perez, Sylvie Tissot and Lou Vettier and the talk is based on the following paper https://arxiv.org/abs/2211.16324

Séminaire des membres non-permanents
Vendredi 19 mai 2023, 11 heures, 3052 and Zoom link
Herman Goulet-Ouellet (IRIF) An introduction to free profinite monoids

The aim of this talk is to introduce free profinite monoids as a fundamental tool to study rational languages and automata.

From an algebraic perspective, running a finite-state automaton is like computing images under a morphism going to a finite monoid. Taken simultaneously, these morphic images act like a fingerprint which can tell apart words from each other. This also defines a metric, the profinite distance, based on how large monoids need to be in order to separate two given words.

The space defined by this metric is discrete and infinite, hence full of holes. Its metric completion is called the free profinite monoid. It is an intriguing object in which algebra, topology and combinatorics interact in subtle ways. Topologically, it looks like the Cantor space, but it also has an algebraic structure which extends the usual word concatenation.

Inside the free profinite monoid, rational languages turn into clopen subsets by topological closure, while clopen subsets turn back into rational languages by intersection. This back-and-fourth adds to the three classical representations of regular languages – automata, regexes and morphisms – a fourth one, which is purely topological.

Séminaire des membres non-permanents
Jeudi 11 mai 2023, 16 heures, 3052 and Zoom link
Alexandra Rogova Graph databases : how we got here, what they are and how to query them

Graph databases have recently transitioned from being a niche “old school” idea to the cool new paradigm used in biology, machine learning, banking and social network analysis, just to name a few. Because of this diversity, many data models and query languages have been developed and studied by different communities with few links to one another. In 2019, an ISO committee approved a project to create GQL, a standard Graph Query Language for the “property graph” model. The goal of this talk is to give a (theoretician-friendly) introduction to property graphs and GQL, after a brief review of the historical context that got us here.

Séminaire des membres non-permanents
Jeudi 4 mai 2023, 16 heures, 3052 and Zoom link
Maël Luce Distributed Grover: a quantum advantage in the CONGEST model

Grover algorithm is the second most well-known quantum algorithm after Shor's. If the speedup in complexity it represents is “only” quadratic, its main strength is the generality of its use: finding unknown marked items in a set of mostly unmarked ones, where the set and the marks are arbitrarily defined. In recent years, a distributed version of this algorithm has emerged leading to faster algorithms in the CONGEST model.

In this talk, the basics of quantum computing will first be defined. Afterwards, I will try to give a feel of how the Grover algorithm operates before finally exploring one or two of its applications in the CONGEST model.

Séminaire des membres non-permanents
Jeudi 27 avril 2023, 16 heures, Olympe de Gouges 146 and Zoom link
Arjan Cornelissen Introduction to quantum algorithms

In this talk, I will give an introduction to quantum algorithms. First, I will explain what quantum algorithms are. Then, I will elaborate on a canonical example known as Grover's algorithm, which provides a quadratic improvement in query complexity for the unstructured search problem over the best classical algorithm. If time permits, I will end with a discussion on generalizations of this result.

Séminaire des membres non-permanents
Jeudi 20 avril 2023, 16 heures, Olympe de Gouges 146 and Zoom link
Daniel Vaz An Introduction to Treewidth and Parameterized Algorithms

NP-hard problems have many applications in our society, from optimizing industry processes, to transports, and even biology. While we cannot efficiently solve every instance of these problems, we sometimes find that the most common instances have simpler structure, which we can exploit to obtain faster algorithms. Parameterized algorithms focus on solving instances instances where some parameter of the instance is low, such as the maximum degree (of the input graph); the number of dimensions (for input data in the Euclidean space); or the size of the solution.

In this talk, we will give an introduction to parameterized algorithms, starting by some simple examples of problems where this approach is useful. Then, we will turn our focus to a specific parameter, called treewidth, which has lead to many new algorithms and also has some practical applications. We will start by looking at an intuitive view of what treewidth is, and how that intuition can be formally defined; then, we will look at how the treewidth of a graph can be computed; and finally, how we can solve problems in graphs with low treewidth.

This will be an introductory talk, so no prior knowledge is needed!

Séminaire des membres non-permanents
Vendredi 14 avril 2023, 11 heures, 3052 and Zoom link
Enrique Román Calvo But… what is verification? (A short introduction to distributed databases and DPOR)

Program verification is a quite well-known field in computer science research that is still obscure for those out of it. This talk presents one particular case, verification of concurrent programs under weak transactional isolation levels via Dynamic Partial Order Reduction (DPOR). I will first introduce the concept of verification, followed by an introduction of weak memory models and distributed databases using several simple examples. Finally, I will explain dynamic partial order reduction (DPOR) technique used to solve our problem and elaborate on our results. No prior knowledge is expected!

Séminaire des membres non-permanents
Vendredi 7 avril 2023, 11 heures, 3052 and Zoom link
Avinandan Das Efficient Semi-Streaming Algorithms and Lower Bounds for Degeneracy Based Graph Coloring

In this talk, we will introduce a space constrained model of computation, aka the Streaming Model. In particular, we will look at a simple algorithm for degeneracy based graph coloring in this model, which was proposed in 2019 and is currently the state of the art (in terms of number of colors used). We will complement the algorithm with a corresponding lower bound which uses a reduction to the problem of indexing in communication complexity and end with an open problem.

No prerequisite is assumed and every notion used will defined in the talk.

This presentation is based on the paper “Graph Coloring via Degeneracy in Streaming and Other Space-Conscious Models” by Suman Kalyan Bera, Amit Chakrabarti and Prantar Ghosh.

Séminaire des membres non-permanents
Jeudi 30 mars 2023, 16 heures, 3052 and Zoom link
Shamisa Nematollahi Submodular Maximization Problem

The study of combinatorial optimization problems with a submodular objective has attracted much attention in recent years. Such problems are important in both theory and practice because their objective functions are very general. A few examples of such functions include cuts functions of graphs and hypergraphs, rank functions of matroids, and covering functions.

Let $N = {u_1, u_2, ..., u_n}$ be a ground set of elements, A function $F : 2^{\mathcal{N}} \to R_{\geq 0}$ is submodular if for every $A \subset B \subset \mathcal{N}$ and $u \in \mathcal{N} \setminus B$, $F(A\cup\{u\})−F(A) \geq F (B \cup \{u\}) − F (B)$. Since the submodular maximization problem is NP-hard, we will discuss some important approximation algorithms of the constrained versions of the problem in both monotone and non-monotone cases.

Séminaire des membres non-permanents
Vendredi 24 mars 2023, 11 heures, 3052 and Zoom link
Robin Vacus Introduction to Game-Theory: Braess-like paradoxes

One of the most fascinating phenomena in game theory is the Braess paradox, which occurs when adding an additional route to a network leads to increased congestion and travel times for everyone. In this talk, after introducing some basic concepts and presenting the paradox, I will describe a few other scenarios in which improving the productivity of individuals counter-intuitively leads to degraded group productivity.

Séminaire des membres non-permanents
Jeudi 16 mars 2023, 16 heures, 3052 and Zoom link
Clément Ducros Secure Multiparty Computation: a brief introduction

Secure Multiparty Computation (MPC) is a set of techniques that allows n distrustful parties to perform a computation, e.g. f(x_1,…,x_n), without revealing anything about their private values x_1,…,x_n. In this talk, I want to present some basic but fundamental principles and techniques of the field - ideal vs. real world / secret sharing / Multiplication Triples - and give a taste of what MPC looks like. It will also serve as an introduction to a future talk on my research into pseudorandom correlation generators.

No prior knowledge is required.

Séminaire des membres non-permanents
Jeudi 9 mars 2023, 16 heures, 3052 and Zoom link
Dániel Szabó Simplicial complexes - an introduction to Topological Data Analysis

Topological Data Analysis (TDA) has recently been getting more and more attention. It models a data set as a simplicial complex, a generalisation of a graph, that is a collection of points having higher order relations among each other. This talk aims at introducing simplicial complexes and some related notions, as well as presenting some algorithmic aspects of calculating and approximating the so-called Betti numbers (the number of high dimensional “holes” in the complex) that can be used to characterise the underlying data set.

Séminaire des membres non-permanents
Jeudi 16 février 2023, 16 heures, 3052 and Zoom link
Klara Nosan Identity Testing for Radical Expressions

Identity testing is a fundamental problem in algorithmic algebra which asks to test equality of two given algebraic expressions. The identity testing problem has many versions according to the syntactic representation of expressions and the ring in which evaluation is carried out. I will introduce different versions of the problem, and then focus on Radical Identity Testing (RIT): Given an algebraic circuit representing a polynomial $f\in \mathbb{Z}[x_1, \dots, x_k]$ and nonnegative integers $a_1, \dots, a_k$ and $d_1, \dots,$ $d_k$, written in binary, test whether the polynomial vanishes at the real radicals $\sqrt[d_1]{a_1}, \dots,\sqrt[d_k]{a_k}$, i.e., test whether $f(\sqrt[d_1]{a_1}, \dots, \sqrt[d_k]{a_k}) = 0$.

In a LICS’22 paper we showed that the RIT problem is in coNP assuming the Generalised Riemann Hypothesis (GRH), improving on the straightforward PSPACE upper bound obtained by reduction to the existential theory of reals. We also considered a restricted version, called 2-RIT, where the radicals are square roots of prime numbers; and showed that 2-RIT is in coRP assuming GRH and in coNP unconditionally.

Our proof relies on theorems from algebraic and analytic number theory, such as the Chebotarev density theorem and quadratic reciprocity, however, no prior knowledge on algebraic circuits, identity testing, or any of the underlying math will be required!

Séminaire des membres non-permanents
Jeudi 2 février 2023, 16 heures, 3052 and Zoom link
Aymeric Walch The categorical semantic iceberg finally explained

Denotational semantic is a field which consists in studying computation without computing. That is, a program P of type int → int can be seen on a high level as a function from the integers to the integers.

After a quick review of the idea behind denotational semantic, we will show that the word “denotational” can in fact be replaced by the word “categorical”. A program will not be interpreted as a mere function, but rather as a morphism in some category. This enlargement of perspective allows us to consider a lot more interesting interpretations for programs: relations, games, probability kernels…

We will then cover the basic categorical ingredients that makes a category a good candidate for interpreting computation. That is, a category must handle tupling and curryfication. If the time allows for it, we will then quickly introduce how those categorical ideas lead to the development of linear logic.

This talk *will not* assume any prior knowledge in category theory nor in denotational semantic.

Séminaire des membres non-permanents
Jeudi 26 janvier 2023, 16 heures, 3052 and Zoom link
Filippo Brunelli Computing minimum-cost temporal walks

In a temporal graph, each edge is available at specific points in time. Such an availability is often represented by a ``temporal edge'' that can be traversed from its tail only at a specific departure time, for arriving in its head after a specific travel time. In such a graph, the connectivity from one node to another is naturally captured by the existence of a temporal path where temporal edges can be traversed one after the other. When imposing constraints on how much time it is possible to wait at a node in-between two temporal edges, it then becomes interesting to consider temporal walks where it is allowed to visit several times the same node, possibly at different times.

I will introduce the problem of computing minimum-cost temporal walks, using an algebraic framework for manipulating abstract costs enabling the optimization of a large variety of criteria. I will then present some algorithmic results recently obtained together with my supervisor (Laurent Viennot).

No prior knowledge of graph theory is going to be required.

Séminaire des membres non-permanents
Jeudi 19 janvier 2023, 16 heures, 3052 and Zoom link
Christoph Egger From Complexity to Cryptography: Key Agreement in Bounded Space

In this talk I want to show how sometimes breakthrough results in complexity can almost directly provide us with interesting new ways of doing cryptography and how we then build more interesting cryptography from it. My aim is to be accessible to all IRIF students.

Concretely we start from the space-time lower bound for (parity-)learning by Raz (FOCS'16) – which we are using in a blackbox manner – and see how this almost directly gives us encryption. In a second step we will explore key agreement using the same building blocks as proposed by Guan and Zhandry (EuroCrypt'19).

Séminaire des membres non-permanents
Jeudi 12 janvier 2023, 16 heures, 3052 and Zoom link
Yaëlle Vinçont Combining fuzzing and symbolic methods for smarter automated test generation

Fuzzing is nowadays one of the most popular test generation technique. It is very good at quickly exploring the surface of a program, using quick automatic generation of test cases, sometimes guided through measures such as coverage.

However, if a program contains specific conditions (such as x = 0x42, where x is a user input), the probability of a fuzzer generating a solution is rather low.

During my thesis, we tried to improve AFL, an existing fuzzer, by combining it with a symbolic analysis. This analysis analyzes traces of generated test cases, in order to identify such conditions (e.g, it would identify that input[0] = 0x0042). From this information we deduce under-approximated path predicates, which we call “easily enumerable”. The solutions to those path predicates are then generated by our fuzzer, which we modified to this purpose, rather than an SMT solver.

This work resulted in a tool, called Confuzz, combining a modified AFL and the symbolic analysis written as a plug-in to the Binsec binary code analysis platform.


Année 2022

Séminaire des membres non-permanents
Jeudi 8 décembre 2022, 16 heures, 3052 and Zoom link
Srinidhi N Domain specific language for Testing consensus implementations

I will introduce some consensus protocols and give an overview of some of the implementations. Following that, I will introduce what are the existing approaches to testing the implementations and then explain our approach which is akin to unit testing.

No prior knowledge of distributed systems/algorithms is required.

Séminaire des membres non-permanents
Jeudi 24 novembre 2022, 16 heures, 3052 and Zoom link
Esaïe Bauer Method of analytic tableaux for first-order logic

I will give an introduction to first order logic and proof theory in order to present a proof-search algorithm called “Method of analytic tableaux”. I will take this opportunity to talk about nice properties of proof theory and sequent calculus. The talk is more or less a lecture of the book “Introduction à la logique : Théorie de la démonstration” from David, Nour and Raffalli. It will not be about research I am currently working on and therefore should be more accessible to everyone. Looking forward to see you there!

Séminaire des membres non-permanents
Jeudi 17 novembre 2022, 16 heures, 3052 and Zoom link
Sander Gribling Quantum query complexity

Everything you always wanted to know (but were afraid to ask): What is it? Why should we care? How do we deal with it? No prior knowledge of quantum computing is required.

Séminaire des membres non-permanents
Jeudi 10 novembre 2022, 16 heures, 3052 and Zoom link
El Mehdi Cherradi ($\infty$-)Categorical semantic of type theory: an introduction

The Curry-Howard correspondence is a very well-known result among (theoretical) computer scientists. However, the link it establishes between programs and proofs has also been extended by Lambek to a certain class of categories. As such, from the perspective that category theory provides a foundational framework for reasoning and logic, it is interesting to identify the underlying categorical structure of models of a given type theory. While the connection is fairly well-understood for intensional flavor of type theory following the work of Hofmann, it is notable that the extension to homotopy type theory is more recent and still incomplete. The goal of this talk is to introduce the basic concepts of the so-called categorical semantic of type theory and its challenging homotopy counterpart.

Séminaire des membres non-permanents
Jeudi 3 novembre 2022, 16 heures, 3052
Mouna Safir Agreement Problems: Optimal Algorithm for Synchronous Byzantine Agreement

The agreement problems has been extensively studied in distributed computing. Beyond the practical interest of this problem, particularly regarding fault-tolerant distributed computing, one of the main reasons behind the focus on agreement problem is the fact that it can be used to define and compare computational power properties of systems. In this presentation I will introduce two agreement problems: Byzantine General problem and k-set Agreement. In k-set agreement, each process must decide on value such that no more than k different values are decided by processes. In addition, the processes must guarantee a validity condition according to the failure models of the processes. Therefore, with crash process failures, the validity condition ensures that the decided values are initial values proposed by processes. In the case where k=1, the k-set agreement is the very classical consensus problem which is fundamental for fault tolerant distributed algorithms.

Séminaire des membres non-permanents
Jeudi 27 octobre 2022, 16 heures, 3052
All Non-Permanent Members Introductory session

This will be an introductory session where we invite all (new and old!) non-permanent members to come and talk about their research interests. Each talk should be 2-5 minutes long, and understandable by everyone.

Séminaire des membres non-permanents
Jeudi 13 octobre 2022, 11 heures, 3052
Amanda Burcroff (Harvard University) Fundamentals of Hyperplane Arrangements

Imagine you are high-dimensional being with scissors that can make d-dimensional cuts into (d+1)-dimensional objects. How many regions can you split an object into with a fixed number of cuts? What if all of your cuts must pass through the center of the object? Are there special patterns of cuts with nice properties? We will study these questions and more through a brief introduction to hyperplane arrangements. Hyperplane arrangements are of much interest to combinatorialists, and as they encode the structure of many important combinatorial problems. We will also briefly discuss how hyperplane arrangements have played a fundamental role in the understanding of certain neural networks.

Séminaire des membres non-permanents
Jeudi 6 octobre 2022, 16 heures, 3052 and Zoom link
Adrienne Lancelot (IRIF) Equivalences of Programs in the lambda calculus

In the study of programming languages, an essential point is the ability to state program equivalence, whether it is to reason abstractly or to establish that some program transformations, used typically when compiling programs, preserve the behavior of programs. The topic of this talk is the study of program equivalence for the case of programs expressed as terms of the λ-calculus, seen as a mathematical model of functional programming languages. We will survey existing program equivalences and focus on normal form bisimulations, in different variants of the lambda calculus. The lambda calculus was first introduced as a way to represent computable functions, with the Call-by-Name variant which has been extensively studied. Nowadays, functional programming languages use mostly the Call-by-Value variant (OCamL) and some the Call-by-Need variant (Haskell). In Call-by-Name, normal form bisimulations yield very satisfactory results. Unfortunately, these do not export to Call-by-Value. Part of my thesis work will be trying to find a satisfactory program equivalence in Call-by-Value.

The previous talk by Victor Arrial is a nice introduction to this talk but concepts tied to the lambda calculus (and its variants) will be re-explained. We will also need the (more generic) concept of co-induction to form program equivalences, which will be briefly explained as well.

Séminaire des membres non-permanents
Jeudi 22 septembre 2022, 16 heures, 3052 and Zoom link
Victor Arrial (IRIF) Introduction to Lambda-Calculus and Quantitative Typing Systems

This talk is planned to be an informal (very much non-exhaustive) introduction to lambda calculus (from a syntactical point of view). The idea is to give intuition on the calculus and two different reduction strategies (Call-by-Value and Call-by-Name). We will then briefly explore/compare three typing systems (simple types, graded linear types, multitypes). It is intended as an introduction to a forthcoming talk on “Quantitative Inhabitation in Call-by-Push-Value” (non-permanents seminar).

Séminaire des membres non-permanents
Jeudi 15 septembre 2022, 16 heures, 3052 and Zoom link
Vincent Moreau (IRIF) Categories for the uninitiated

The talk will be a 1-hour introductory session on category theory accessible to everyone. We introduce categories as generalizations of ordered sets and then focus on the notion of universal property and show through examples how such properties can be used to describe behaviours in different areas of mathematics in a unified way. No prerequisites.

Séminaire des membres non-permanents
Jeudi 2 juin 2022, 16 heures, Salle 3052
Avinandan Das Streaming and computing Frequency Moments in Streaming.

In this talk, we will talk about the Data Stream Model of computation. In this model, the input arrives as a stream of items and the workspace of the algorithm is very low and therefore, the whole input cannot be stored in the memory. Due to space constraints, data streaming algorithms use elegant and non trivial randomization techniques to store summary of the input seen so far. The model is inspired by the advent of data explosion, where it is impossible to store all of the data in the memory and also by database applications, where random access cost is high. We will see algorithms for frequency moments computation ($F_0$ and $F_2$) over a stream of elements, which actually kickstarted the field of data stream algorithms. This talk is based on lecture notes from the course “Communication Complexity (for Algorithm Designers)” by Tim Roughgarden (http://timroughgarden.org/notes.html).

Séminaire des membres non-permanents
Jeudi 19 mai 2022, 16 heures, Salle 1007
Lucía Rossi (University of Leoben, Austria) Limit words for N-continued fractions

We begin by introducing Sturmian words, which are infinite words on a two letter alphabet. An infinite word ω is said to be Sturmain if, for any given n, there exist exactly n+1 distinct subwords of ω of length n. They are, in some sense, the simplest possible non-trivial words. Geometrically, they correspond to a cutting sequence obtained from a line of irrational slope on a square grid, and there is a very nice correspondence between the coding sequence of ω and the continued fraction expansion of the slope. Given N ≥ 1 and x ∈ [0, 1] \ Q, an N-continued fraction expansion of x is defined analogously as the classical continued fraction, but with the numerators being all equal to N. An infinite word ω(x, N) on a two letter alphabet is obtained as a limit word of a sequence of substitutions, which we call an NCF word. When N = 1, we find a Sturmian word. We present some combinatorial and analytic results obtained for NCF words, namely: balance properties, letter frequency, factor complexity. This is joint work with Niels Langeveld and Jörg Thuswaldner.

Séminaire des membres non-permanents
Jeudi 12 mai 2022, 16 heures, Salle 1007
Daniel Szabo Quantum algorithms for the longest common substring problem

The longest common substring problem (LCS) is one of the most fundamental string problems. We look at the decision version of LCS: given two texts s and t and a parameter d we want to find out if there is a string of length d that appears as a substring in both s and t. Its classical complexity is well understood: it is linear in the length of s and t, which we denote by n. In the quantum setting, two algorithms can be combined to get the best known upper bound: one has query (and time) complexity O(n^(2/3)) for any value of d; and the other one uses O(n/sqrt(d)) queries. In the talk I will try to present the main ideas behind these results in such a way that people without much knowledge on quantum computing can follow too.

Séminaire des membres non-permanents
Jeudi 28 avril 2022, 16 heures, Salle 3052
Félix Castro An interpretation of E-HA^ω inside HA^ω

HA^ω (Higher Type Arithmetic) is a first order many sorted theory. It is a conservative extension of HA (Heyting Arithmetic a.k.a the intuitionistic version of Peano Arithmetic) obtained by extending the syntax of terms to all the System T : the objects of interest here are the functionals of “higher types”. While equality between natural numbers is well understood (it is canonical and decidable), how equality between functionals can be defined ? From this question, different versions of HA^ω arise : an extensional version (E-HA^ω) and an intentional version (I-HA^ω).

Séminaire des membres non-permanents
Jeudi 24 mars 2022, 16 heures 30, Salle 3052
Patrick Lambein-Monette Average consensus in spite of dynamic interactions

Picture a networked system of autonomous agents, each starting with some initial value. In the /average consensus/ problem, the agents should collectively compute the arithmetic mean of those values, through local interactions over a connected network.

Classically, this problem is considered in a setting where the agents hold no unique identifier, and do not start knowing a bound over the size of the system. These restrictive assumptions give rise to two major obstacles to our problem. First, it is generally impossible for an agent to detect that it has reached the desired answer; as such, we only expect the system to asymptotically converge towards the average, rather than to irrevocably decide on it. Second, it is generally impossible to properly account for the multiplicities of the initial values; we therefore restrict our considerations to bidirectional communication links.

For fixed bidirectional networks, an efficient solution is to be found in the /Metropolis/ averaging algorithm, first proposed by Xiao and colleagues in 2005. However, when moving to consider /dynamic/ networks – i.e., where the communication links can arbitrarily change at each step of the execution – the Metropolis rule isn't algorithmic, in the sense that it requires the agents cannot themselves gather all the information required to implement the rule. Other average consensus protocols proposed in the literature fare no better for the same reasons.

We propose the /MaxMetropolis/ rule, an adaptation of the Metropolis rule that is history-dependent, and admits a totally decentralized and local implementation. Over bidirectional dynamic networks with $n$ agents and connectivity delay $B$, $O(B n^4 log n/r)$ communication rounds are required to achieve a relative disagreement of $r > 0$ over the value of the average. This is the first truly distributed average consensus algorithm for bidirectional dynamic networks.

Séminaire des membres non-permanents
Jeudi 10 mars 2022, 16 heures, Salle 3052
Robin Vacus Early Adapting to Trends: Self-Stabilizing Information Spread using Passive Communication

How to efficiently and reliably spread information in a system is one of the most fundamental problems in distributed computing as well as in the animal world. In this talk, we will consider the self-stabilizing bit-dissemination problem, motivated by biological scenarios, in the extremely constrained model of passive communication.

Séminaire des membres non-permanents
Jeudi 24 février 2022, 16 heures, Salle 3052
Filippo Brunelli Walk Temporalisation and Reachability Maximisation in Temporal Graphs

In a temporal graph, each edge appears and can be traversed at specific points in time. In such a graph, temporal reachability of one node from another is naturally captured by the existence of a temporal path where edges appear in chronological order. Inspired by the optimisation of bus/metro/tramway schedules in a public transport network, we consider the problem of turning a collection of walks (called trips) in a directed graph into a temporal graph by assigning a starting time to each trip so as to maximise the reachability among pairs of nodes. Each trip represents the trajectory of a vehicle and its edges must be scheduled one right after another. Setting a starting time to the trip thus forces the appearing time of all its edges. We call such a starting time assignment a trip temporalisation.

We will speak about results on the complexity of maximising reachability via trip temporalisation. We will show that the problem is hard to approximate even when we assume the nice property that for each pair of nodes, there exists a trip temporalisation connecting them. On the positive side, we show that there must exist a trip temporalisation connecting a constant fraction of all pairs if we additionally assume symmetry in the trip network.

Séminaire des membres non-permanents
Jeudi 17 février 2022, 16 heures, Salle 3052
Klara Nosan On matrix groups, the Zariski topology and what they both have to do with automata and verification

Finitely generated groups of matrices are fundamental mathematical objects that appear in a wide variety of areas in computer science, including algebraic complexity theory, quantum computation, dynamical systems, graph theory, control theory, and program verification. Unfortunately, matrix groups are challenging from the algorithmic point of view, with many natural problems being undecidable. In order to get a better handle on a finitely generated matrix group, it turns out to be worth over-approximating it by its Zariski closure, which admits a finite representation.

This talk will be a gentle introduction to (computing) the Zariski closure of finitely generated matrix groups with examples of applications in automata theory and program verification. We will describe an existing algorithm for computing the closure due to Derksen, Jeandel and Koiran. We will conclude by discussing our result, which is to obtain an upper bound on the degree of the polynomials that define the Zariski closure. Having an a priori bound allows us to give a simple algorithm for the problem, via linear algebra, similar to Karr's algorithm for obtaining affine invariants for affine programs.


Année 2021

Séminaire des membres non-permanents
Jeudi 16 décembre 2021, 11 heures, Salle 3052
Abhishek De & Pierre Meyer Multi-party encrypted communication between ASD, ASV and PPS

Talk 1 (Abhishek): How can someone from PPS chat up someone from ASD or ASV?

PPS looks at abstractions of programming languages and studies logics motivated to better understand these abstractions. How can tools developed here be used in other fields like automata theory and complexity theory? In this talk, I will give some ideas roughly along the lines of implicit complexity and hope to forge further collaborations between the 3rd floor and 4th floor.

Talk 2 (Pierre): What does it take to hide patterns of communication?

Secure Multiparty Computation (MPC) allows N mutually distrusting parties to perform some computation f(x_1,…,x_N) without having to reveal anything about their private inputs x_1,…,x_N beyond what is revealed by the output of the computation itself. Making sure that “adversaries”, which are internal to the system rather than external, cannot learn more information than they should is a well-understood task in the setting where any pair of parties can communicate directly (and privately). However, in many scenarios, setting up a complete communication network is impractical (e.g. too expensive) or impossible (e.g. some parties may outright refuse to communicate with some others). Therefore, we consider the more realistic setting where the parties are nodes in some incomplete graph, and can communicate only along the edges. In fact, knowledge of this network could be kept private too: each party knows who they are talking to but they do not need to know the metadata of how others are communicating, which may be sensitive information. There are two difficulties to achieving this extra privacy requirement: (1) the MPC protocol must be run even if the each party only knows their local view of the network (i.e. their neighbourhood), and (2) the MPC protocol should reveal nothing more about the graph.

In this talk, we will try and understand how hard this task is by relating it to a foundational hierarchy of cryptographic primitives: - Secure Communication: Two parties need to communicate privately even in the presence of an external eavesdropper monitoring all their interactions. - Secure Computation: Two parties need to compute some function without trusting each other with their inputs. Prerequisites: No background in cryptography is required.

Séminaire des membres non-permanents
Mercredi 24 novembre 2021, 11 heures, Salle 3052
Corentin Henriet & Simon Mauras Fighting fish and assigning students

Talk 1 (Corentin): Combinatorics of fighting fishes and related structures

Fighting fishes are combinatorial objects generalizing parallelogram polyominoes introduced in 2016 by Duchi et al. The enumeration of these objects with respect to their natural parameter of size (the half-perimeter) leads to a sequence that counts also other objects : two-stack sortable permutations, non-separable planar rooted maps, synchronized intervals of the Tamari lattice. In this presentation, I will define some bijections between fighting fishes and other objects that preserve a lot of structure and statistics, and I will give some perspectives about the generalization of considered objects and bijections.

Talk 2 (Simon): Random models for stable matching

In a two sided matching market, two types of agents have preferences over one another. Examples include college admissions (students and colleges), residency programs (doctors and hospitals), job markets (workers and jobs) and, in the classical analogy, stable marriages (men and women). In a founding paper, Gale and Shapley introduced the deferred acceptance procedure, where one side proposes and the other disposes, which computes a stable matching. In the worst case, the choice of which side of the market proposes has a big importance, both in terms of outcome (the output matching is optimal for the proposing side) and truthfulness (the receiving side might have incentives to lie). We will show that things are much nicer in the average case. Assuming that preferences of agents are drawn from certain distributions, then each agent receives with high probability the same allocation in the two variants of deferred acceptance.

Séminaire des membres non-permanents
Mercredi 2 juin 2021, 16 heures, Salle 3052
Quentin Ferro (IRIF) Distributed Recoloring using the LOCAL Model

Recoloring is a reconfiguration problem : given a graph and two proper coloring of this graph, how to recolor from one coloring to the other by a series of elementary changes ? The talk will be based on the Distributed Recoloring paper from Marthe Bonamy, Paul Ouvrard, Mikaël Rabie, Jukka Suomela, and Jara Uitto (Disc 2018) which introduced the notion of distributed recoloring as follow : the input graph represent a network of computers that need to be recolored. Each node know its input color and its target color. Nodes are allowed to exchange messages with each other synchronously and, given rounds of messages, each node have to output its recoloring schedule, indicating when the node changes its color and to which color. The recoloring schedules have to be globally consistent so that the graph remains properly colored at each point, and we require that adjacent nodes do not change their colors simultaneously. This paper gave a lot of results for different situations of coloring (different types of graph, different number of color, different number of extra color), particularly problems with 1 extra colors, and left some open questions. I will present some results we have on some of those open questions.

Séminaire des membres non-permanents
Mercredi 26 mai 2021, 16 heures, Salle 3052
Avinandan Das (IRIF) Combinatorial Proof for Chernoff-Hoeffding Concentration Bound

In this talk, I will give a combinatorial proof of the Chernoff-Hoeffding concentration bound, which says that the sum of independent $\{0,1\}$-valued random variables is highly concentrated around the expected value. Unlike the standard proofs, this proof does not use the method of higher moments, but rather uses a simple and intuitive counting argument. In addition, this proof is constructive in the following sense: if the sum of the given random variables is not concentrated around the expectation, then we can efficiently find (with high probability) a subset of the random variables that are statistically dependent. This talk is based on the paper “Constructive Proofs of Concentration Bounds” by Russell Impagliazzo and Valentine Kabanets.


Année 2020

Séminaire des membres non-permanents
Mercredi 2 décembre 2020, 11 heures, Online
Phd Students Welcome session!

Séminaire des membres non-permanents
Mercredi 6 mai 2020, 11 heures, Online
Cédric Ho Thanh (IRIF) An introduction to Docker

This presentation aims to be a quick introduction to docker: its role, inner workings, ecosystem, and most importantly, how to use it. We will start with a little bit of theory, and swiftly move to a demo. Some notions about operating systems might be beneficial, but I will try to review what we need.

Séminaire des membres non-permanents
Mercredi 22 avril 2020, 11 heures, Online
Simon Mauras (IRIF) How to aggregate top-lists

A top-list is a possibly incomplete ranking of elements: only a subset of the elements are ranked, with all unranked elements tied for last. Top-list aggregation takes as input a collection of top-lists and aggregates them into a single complete output ranking, aiming to minimize the number of upsets (pairs ranked in opposite order in the input and in the output).

This talk will start with a quick survey on rank aggregation (the special case where every input list is a complete ranking of the elements), its relation to feedback arc sets in directed graphs, NP-Hardness, and approximation algorithms. Then we will discuss how such results can be extended to the aggregation of top-lists.

Preprint available: https://arxiv.org/abs/1811.01537

Séminaire des membres non-permanents
Mercredi 15 avril 2020, 11 heures, Online
Chaitanya Leena Subramaniam (IRIF) The plus-construction for sheaves and factorisation systems

Sheaves are a fundamental kind of algebraic structure in mathematics, and iterating the so-called plus-construction is a well known process of turning a presheaf into a sheaf.

However, the plus-construction makes sense in much more generality than sheaves, and a result (joint with M. Anel) shows that it is in fact closely related to orthogonal factorisation systems on a category. Indeed, it can be used to construct such factorisation systems.

This has many applications, including in dependent type theory, where it has a fundamental application to modalities.

The talk will be a gentle introduction to the plus-construction and its various examples.

Séminaire des membres non-permanents
Mercredi 8 avril 2020, 11 heures, Online
Nicolas Jeannerod (IRIF) Analysing installation scenarios of Debian packages

Debian GNU/Linux is a Linux distribution composed of free and open-source software. It is heavily used all over the world as an operating system for personal computers and servers, and is the basis for many other distributions.

Deban currently includes more than 28 thousand maintainer scripts, almost all of them written in POSIX shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for system maintenance. While Debian policy provides guidance for package maintainers producing the scripts, few tools exist to check the compliance of a script to it.

This presentation reports on the application of a formal verification approach based on symbolic execution to find violations of some non-trivial properties required by Debian policy in maintainer scripts. We present our methodology and give an overview of the toolchain. We focus in particular on the tree logics used to represent symbolically a file system transformation, and the use of such a logic in the symbolic engine.

https://bbb1.math.univ-paris-diderot.fr/b/sim-yez-k3e

Séminaire des membres non-permanents
Mercredi 1 avril 2020, 11 heures, Online
Simona Etinski (IRIF & INRIA) Stern's Zero Knowledge Identification Scheme

In the first part of the talk, I will present the class of interactive proofs (IP) and special property of some of the interactive proofs called zero-knowledge. Public and private coin methods will also be introduced as they play a major role in most of the interactive proofs. The second part of the talk will concern Stern's identification scheme: a zero-knowledge interactive proof that enables one party to prove its identity to the other party without revealing any further information about it. Relying on the syndrome decoding problem, which is believed to be NP-complete, the scheme is considered to be post-quantum and thus a valid candidate for identification schemes to be used long-term. Nevertheless, the rather high communication complexity prevents Stern's scheme from being widely used at the moment and thus poses an issue to address. Some of the recent results and suggested future directions in addressing this issue will be presented in this talk.

https://bbb1.math.univ-paris-diderot.fr/b/sim-yez-k3e

Séminaire des membres non-permanents
Mercredi 25 mars 2020, 11 heures, Online
Nguyễn Lê Thành Dũng (LIPN) Aperiodicity in a non-commutative logic

We give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. Since this work is at the interface of two areas, namely automata theory and programming languages, the talk will assume very little background knowledge and recall the prerequisites for both. I will also present our main inspiration: Hillebrand and Kanellakis's little-known characterization of regular languages in the simply typed λ-calculus (LICS'96). This is a joint work with Pierre Pradic (Oxford); preprint available at https://hal.archives-ouvertes.fr/hal-02476219/document

https://bbb1.math.univ-paris-diderot.fr/b/sim-yez-k3e

Séminaire des membres non-permanents
Lundi 2 mars 2020, 15 heures, Salle 3014
Pierre Cagne Les symmétries des sphères en fondations univalentes


Année 2019

Séminaire des membres non-permanents
Mercredi 27 novembre 2019, 11 heures, Salle 3052
(Old) Phd Students Return of the PhD Seminar

Every new/old PhD student is invited to come and talk about her/his research interests.

Each talk will be 2-5 minutes long, and should be understandable by everyone.

Séminaire des membres non-permanents
Mercredi 20 novembre 2019, 11 heures, Salle 3052
Pierre Ohlmann (IRIF) Controlling a random population

Bertrand et al. (2017) introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min- cut theorem, and of the theory of regular cost functions.

Séminaire des membres non-permanents
Mercredi 13 novembre 2019, 11 heures, Salle 3052
(New) Phd Students The PhD Seminar strikes back

Every new/old PhD student is invited to come and talk about her/his research interests.

Each talk will be 2-5 minutes long, without any slides, and should be understandable by everyone

Séminaire des membres non-permanents
Mercredi 24 juillet 2019, 11 heures, Salle 3052
Hugo Moeneclaey (IRIF) Toward a Cubical Type Theory Univalent by Definition

Univalent foundations are based on a geometric interpretation of identity types in type theory. We will explain this interpretation, then we will give a brief introduction to Cubical Type Theory and explain why it is useful in this context. Then we will present some ideas from parametricity and sketch how we are trying to use them to build a variant of Cubical Type Theory.

Séminaire des membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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.

Short session

Séminaire des membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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.

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)

Séminaire des membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
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.

Le séminaire sera donné en français.

Séminaire des membres non-permanents
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 membres non-permanents
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 membres non-permanents
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.

These are two newcomers talk, 30 minutes each. The first will be in English, the second in French.


Année 2017

Séminaire des membres non-permanents
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 membres non-permanents
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 membres non-permanents
Mercredi 6 décembre 2017, 11 heures, Salle 3052
Axel Osmond & Yassine Hamoudi ([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 do spatial reasoning, one can rise some ontological and logical suspicions about naive notion of points as they constitute idealized objects with somewhat inaccessible aspects in a constructive and finite point of view. Locales and Frames theories are two deeply entangled realms aimed at rebuilding topology on latticial and categorical foundations, in which usual notions of points, opens, subspaces, separability, compacity… can be reexpressed as first order algebraic properties in latticial context, or both generalized and made constructive.

Formal topology goes further into this last direction, using systems of axioms about coverings as a deductive systems which leads to a type-theoretic flavored, predicative and constructive topology, endowed with multiple and finer notions of points, separability… and suited for 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 membres non-permanents
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 membres non-permanents
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 instead to give a gentle pictorial introduction to the inherent structure of dependent types and how this structure determines what dependent types and dependently-typed programs (or proofs) *mean*.

The focus will be on why this structure naturally leads to homotopy type theory and univalence. As a bonus, and if time permits, there will be some remarks on univalence and extensionality.

Séminaire des membres non-permanents
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 membres non-permanents
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 theorem

In 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 membres non-permanents
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 below

Du forcing à la réalisabilité classique: une nouvelle approche

La 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 Approach

Classical 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 membres non-permanents
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 enumeration

Combinatorial maps (which are embeddings of graphs on surfaces) are well studied objects in combinatorics, which have applications in other domains, such as quantum gravity. The goal is to enumerate them (sometimes exactly, sometimes asymptotically). For this purpose, one can resort to (among other things) bijective or algebraic methods. The algebraic 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 to re-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 I discovered during my Master’s internship.

Gradual Set-Theoretic Types

A static type system can be an extremely powerful tool for a programmer, providing early error detection, and offering strong compile-time guarantees on the behavior of a program. However, compared to dynamic typing, static typing often comes at the expense of development speed and flexibility, as statically- typed code might be more difficult to adapt to changing requirements. Gradual typing is a recent and promising approach that tries to get the best of both worlds, 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 is often either fully dynamic or fully static. We argue that adding full-fledged union and intersection types (a.k.a. set-theoretic types) to a gradual type system solves this issue by making the transition between dynamic typing and static typing smoother.

Séminaire des membres non-permanents
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 membres non-permanents
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 do precalculation in order to reduce query time. A methode is to use Hub Labeling. Hub Labeling works well on road transport network. We will take a look at this methode and introduce the notion of Skeleton Dimension which give an insight on why it works well on road network.

Séminaire des membres non-permanents
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 membres non-permanents
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 type systems), en particulier, les ITS à intersection non-idempotente. Je commencerai par des rappels basiques en lambda-calcul. On verra en quoi la représentation des lambda-termes par des arbres (bien qu'élémentaire) permet de comprendre la façon dont les ITS sont conçus et vérifient naturellement des propriétés que les systèmes de types simples ne peuvent (raisonnablement) pas avoir. Par exemple, dans un ITS, un terme est normalisable (i.e. il termine) ssi il est typable. Par opposition, dans un système de types simples, on aura seulement l'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, la ré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 en lambda-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 de types simples, d'ordre supérieur ou non), la propriété de terminaison (typable dans Sys ⇒ normalisable) est souvent difficile à établir (on doit généralement recourir à un argument dit de réalisabilité, attribué à Tait). Cependant, je présenterai le système R, introduit par Gardner et de de Carvalho, dans lequel l'opérateur d'intersection peut être vu comme non-idempotent et la terminaison repose sur un argument très simple que nous verrons ensemble.

2) Présenter un article (accepté récemment à LICS) traitant de lambda-calcul et de réduction infinitaires et dont voici l'abstract:

Infinitary Intersection Types as Sequences: a New Answer to Klop’s Problem

We provide a type-theoretical characterization of weakly-normalizing terms in an infinitary lambda-calculus. We adapt for this purpose the standard quantitative (with non-idempotent intersections) type assignment system of the lambda-calculus to our infinite calculus. Our work provides a positive answer to a semi-open question known as Klop’s Problem, namely, finding out if there is a type system characterizing the set of hereditary head-normalizing (HHN) lambda-terms. Tatsuta showed in 2007 that HHN could not be characterized by a finite type system. We prove that an infinitary type system endowed with a validity condition called approximability can achieve it. As it turns out, approximability cannot be expressed when intersection is represented by means of multisets. Multisets are then replaced coinductively by sequences of types indexed by integers, thus defining a type system called System S.

Séminaire des membres non-permanents
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 membres non-permanents
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 membres non-permanents
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 membres non-permanents
Mercredi 22 mars 2017, 11 heures, Salle 3052
Gabriel Radanne (PPS team) GADTs gone mild

Generalized Algebraic Data Types, often also called “Poor man's dependent types”, are an extension of regular sum and product types that is available in OCaml and Haskell.

Since their adoption in “mainstream” languages, GADTs have been known for allowing to elegantly write toy typed interpreter at the cost of horrible type error messages and numerous headaches. Or, as Yaron Misky said, “I assumed that it was the kind of nonsense you get when you let compiler writers design your programming language.”.

In this talk, I will present GADTs, what they are, and what useful things we can do with them. This will take us on quite a journey, with some traces of C, a pinch of memory layout, a cameo from pushdown automata and a healthy amount of Prolog. The only requirements will be a passing familiarity with OCaml and the caffeinated beverage of your choice.

Séminaire des membres non-permanents
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 membres non-permanents
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 which in each round, each agent extracts information from few randomly chosen agents. We seek to identify the smallest amount of information revealed in each interaction (message size) that nevertheless allows for efficient and robust computations of fundamental information dissemination tasks. We focus on the Majority Bit Dissemination problem that considers a population of n agents, with a designated subset of source agents. Each source agent holds an input bit and each agent holds an output bit. The goal is to let all agents converge their output bits on the most frequent input bit of the sources (the majority bit). Note that the particular case of a single source agent corresponds to the classical problem of Broadcast (also termed Rumor Spreading). We concentrate on the severe fault-tolerant context of self-stabilization, in which a correct configuration must be reached eventually, despite all agents starting the execution with arbitrary initial states. In particular, the specification of who is a source and what is its initial input bit may be set by an adversary.

We first design a general compiler which can essentially transform any self-stabilizing algorithm with a certain property (called “the bitwise-independence property”) that uses l-bits messages to one that uses only (log l)-bits messages, while paying only a small penalty in the running time. By applying this compiler recursively we then obtain a self-stabilizing Clock Synchronization protocol, in which agents synchronize their clocks modulo some given integer T, within O(log n log T) rounds w.h.p., and using messages that contain 3 bits only. We then employ the new Clock Synchronization tool to obtain a self-stabilizing majority broadcast protocol which converges in O(log n) time, w.h.p., on every initial configuration, provided that the ratio of sources supporting the minority opinion is bounded away from half. Moreover, this protocol also uses only 3 bits per interaction.

Based on joint work with A. Korman and E. Natale.

Séminaire des membres non-permanents
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 between deterministic programs in terms of their small-step semantics. This language-agnostic framework defines the notion of /difference languages/ in which /oracles/—programs that relate small-step executions of pairs of programs written in a same language—can be written, reasonned about and composed.

We illustrate this framework by instantiating it on a toy imperative language and by presenting several /difference languages/ ranging from trivial equivalence-preserving syntactic transformations to characterized semantic differences. Through those examples, we will present the basis of our framework, show how to use it to relate syntactic changes with their effect on semantics, how one can abstract away from the small-step semantics presentation, and discuss the composability of oracles.

Séminaire des membres non-permanents
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 between distributed computing and formal logic. I will illustrate this relatively unexplored area of research by presenting an equivalence result between two very specific systems. The distributed computing side will be represented by a network of identical finite-state machines that communicate in an asynchronous manner, while the formal logic side will be represented by a small fragment of least fixpoint logic (more specifically, a fragment of the modal mu-calculus).