Séminaire des doctorants

Séminaire dans lequel les doctorant.e.s et les stagiaires présentent leur travaux devant une audience moins intimidante puisqu'elle est composée des autres doctorant.e.s, stagiaires et éventuellement post-docs.

Date et lieu : le mercredi à 11h, Sophie Germain

Responsables : Laurent Feuilloley, Nicolas Jeannerod, Théo Zimmermann

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

Mercredi 28 juin 2017 · 11h00 · 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.

Mercredi 14 juin 2017 · 11h00 · Salle 3052

Timo Zijlstra Et 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.

Mercredi 31 mai 2017 · 11h00 · 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.

Mercredi 17 mai 2017 · 11h00 · 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.

Mercredi 03 mai 2017 · 11h00 · 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.

Mercredi 19 avril 2017 · 11h00 · 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.

Mercredi 05 avril 2017 · 11h00 · 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.

Mercredi 22 mars 2017 · 11h00 · 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.

Mercredi 08 mars 2017 · 11h00 · 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).

Mercredi 22 février 2017 · 11h00 · 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.

Mercredi 25 janvier 2017 · 11h00 · 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.

Mercredi 11 janvier 2017 · 11h00 · 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).

Voir les archives sur l'ancien site web : http://www.pps.univ-paris-diderot.fr/~c.jacq/seminaire-thesards