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.

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

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.

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

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

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