BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Google Inc//Google Calendar 70.9054//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
DESCRIPTION:Séminaire des doctorants seminar of IRIF
NAME:Séminaire des doctorants
REFRESH-INTERVAL:PT4H
TIMEZONE-ID:Europe/Paris
X-WR-CALDESC:Séminaire des doctorants seminar of IRIF
X-WR-CALNAME:Séminaire des doctorants
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:Asynchronous Distributed Automata - Fabian Reiter\, Automata and a
pplications Group
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170111T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170111T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:175
DESCRIPTION:The goal of this talk is to raise interest in the connections
between\ndistributed computing and formal logic. I will illustrate this\nr
elatively unexplored area of research by presenting an equivalence\nresult
between two very specific systems. The distributed computing\nside will b
e represented by a network of identical finite-state\nmachines that commun
icate in an asynchronous manner\, while the formal\nlogic side will be rep
resented by a small fragment of least fixpoint\nlogic (more specifically\,
a fragment of the modal mu-calculus).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Oracle-based Differential Operational Semantics (or Explaining pro
gram differences with programs) - Thibaut Girka\, PPS team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170125T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170125T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:176
DESCRIPTION:We present a formal framework to characterize differences betw
een\ndeterministic programs in terms of their small-step semantics. This\n
language-agnostic framework defines the notion of /difference languages/ i
n\nwhich /oracles/—programs that relate small-step executions of pairs o
f programs\nwritten in a same language—can be written\, reasonned about
and composed.\n\nWe illustrate this framework by instantiating it on a toy
imperative\nlanguage and by presenting several /difference languages/ ran
ging from trivial\nequivalence-preserving syntactic transformations to cha
racterized semantic\ndifferences. Through those examples\, we will present
the basis of our\nframework\, show how to use it to relate syntactic chan
ges with their effect on\nsemantics\, how one can abstract away from the s
mall-step semantics\npresentation\, and discuss the composability of oracl
es.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:GADTs gone mild - Gabriel Radanne\, PPS team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170322T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170322T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:195
DESCRIPTION:Generalized Algebraic Data Types\, often also called "Poor man
's\ndependent types"\, are an extension of regular sum and product types t
hat\nis available in OCaml and Haskell.\n\nSince their adoption in "mainst
ream" languages\, GADTs have been known\nfor allowing to elegantly write t
oy typed interpreter at the cost of\nhorrible type error messages and nume
rous headaches. Or\, as Yaron Misky\nsaid\, "I assumed that it was the kin
d of nonsense you get when you let\ncompiler writers design your programmi
ng language.".\n\nIn this talk\, I will present GADTs\, what they are\, an
d what useful\nthings we can do with them. This will take us on quite a jo
urney\, with\nsome traces of C\, a pinch of memory layout\, a cameo from p
ushdown\nautomata and a healthy amount of Prolog. The only requirements wi
ll be a\npassing familiarity with OCaml and the caffeinated beverage of yo
ur choice.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Minimizing Message Size in Stochastic Communication Patterns: Fast
Self-Stabilizing Protocols with 3 bits - Lucas Boczkowski\, Algorithms an
d complexity Group
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170222T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170222T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:196
DESCRIPTION:The talk is based on a paper whose abstract is the following:\
n\nThis paper considers the basic PULL model of communication\, in which\n
in each round\, each agent extracts information from few randomly chosen\n
agents. We seek to identify the smallest amount of information revealed\ni
n each interaction (message size) that nevertheless allows for\nefficient
and robust computations of fundamental information\ndissemination tasks. W
e focus on the Majority Bit Dissemination\nproblem that considers a popula
tion of n agents\, with a designated\nsubset of source agents. Each source
agent holds an input bit and each\nagent holds an output bit. The goal is
to let all agents converge\ntheir output bits on the most frequent input
bit of the sources (the\nmajority bit). Note that the particular case of a
single source agent\ncorresponds to the classical problem of Broadcast (a
lso termed Rumor\nSpreading). We concentrate on the severe fault-tolerant
context of\nself-stabilization\, in which a correct configuration must be
reached\neventually\, despite all agents starting the execution with arbit
rary\ninitial states. In particular\, the specification of who is a source
and\nwhat is its initial input bit may be set by an adversary.\n\nWe firs
t design a general compiler which can essentially transform any\nself-stab
ilizing algorithm with a certain property (called "the\nbitwise-independen
ce property") that uses l-bits messages to one\nthat uses only (log l)-bit
s messages\, while paying only a small\npenalty in the running time. By ap
plying this compiler recursively we\nthen obtain a self-stabilizing Clock
Synchronization protocol\, in\nwhich agents synchronize their clocks modul
o some given integer T\,\nwithin O(log n log T) rounds w.h.p.\, and using
messages\nthat contain 3 bits only. We then employ the new Clock Synchroni
zation\ntool to obtain a self-stabilizing majority broadcast protocol whic
h\nconverges in O(log n) time\, w.h.p.\, on every initial\nconfiguration\,
provided that the ratio of sources supporting the\nminority opinion is bo
unded away from half. Moreover\, this protocol also\nuses only 3 bits per
interaction.\n\nBased on joint work with A. Korman and E. Natale.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Continued Fractions and the Recurrence of Sturmian Words - Pablo E
duardo Rotondo\, Automata and applications Group
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170308T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170308T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:201
DESCRIPTION:In this talk I will present various aspects of Continued Fract
ions\, motivating and explaining their relation to the factors of the so-c
alled Sturmian Words. We conclude by a probabilistic study of the recurren
ce function of Sturmian Words\, which is common work with Brigitte Vallée
(CNRS\, Univ. Caen).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the stability of the Lempel-Ziv compression algorithm - Guillau
me Lagarde\, Automata and applications Group
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170405T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170405T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:209
DESCRIPTION:LZ78 is a very simple lossless data compression algorithm publ
ished by Abraham Lempel and Jacob Ziv in 1978. It is fair enough to expect
a certain stability from a data compression algorithm against small pertu
rbation on the input. In this direction\, Jack Lutz among with others aske
d the following question\, so-called "the one-bit catastrophe": given an i
nfinite word w\, can the compression ratio of w be different from 1w? In t
his presentation\, I will give some results in this fashion\; in particula
r I would like to give the intuition of the fact that a catastrophe can in
deed occur in LZ78.\nJoint work with Sylvain Perifel.\n\nThe presentation
will just use basic combinatorics.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lawvere’s hyperdoctrines and notions of equality - Pierre Cagne\
, PPS team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170419T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170419T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:220
DESCRIPTION:This talk will present hyperdoctrines\, a widget invented by L
awvere 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 theo
ry: structural rules\, logical rules\, quantifier rules\, equality rules\,
etc. As a welcomed side effect\, it questions the legitimacy of such rule
s. In particular\, we will take some time to study the equality and the re
levance 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 typ
e theory”\, by which is roughly meant a type theory in which paths betwe
en terms are not necessarily reversible.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Quantum\, a look through nonlocality - Alexandre Nolin\, Algorithm
s and complexity Group
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170503T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170503T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:229
DESCRIPTION:In this talk I will try to give an introduction to the mathema
tical framework of quantum computing\, completely disconnected of the unde
rlying theory of quantum physics. After an exposition of a circuit model f
or quantum computing\, we will split those circuits into two parts (the in
famous Alice and Bob) and talk about the behaviours of those bipartite sys
tems\, more specifically somewhat counter-intuitive phenomenons like entan
glement and nonlocality. Finally\, we will see how those phenomenons are r
elevant in the study of communication complexity\, and discuss recent resu
lts.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:An Introduction to Intersection Type Systems\, and a New Answer t
o Klop's Problem - Pierre Vial\, PPS team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170517T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170517T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:249
DESCRIPTION:Although the following abstract is (mostly) in French\, the ta
lk will be in English if there are non-French speakers in the room.\n\nL'e
xposé aura deux buts:\n\n1) Présenter les systèmes de types-intersectio
n (ITS\, intersection type\nsystems)\, en particulier\, les ITS à interse
ction non-idempotente.\nJe commencerai par des rappels basiques en lambda-
calcul. On verra en\nquoi la représentation des lambda-termes par des arb
res (bien\nqu'élémentaire) permet de comprendre la façon dont les ITS s
ont conçus\net vérifient naturellement des propriétés que les système
s de types\nsimples ne peuvent (raisonnablement) pas avoir. Par exemple\,
dans un\nITS\, un terme est normalisable (i.e. il termine) ssi il est typa
ble. Par\nopposition\, dans un système de types simples\, on aura seuleme
nt\nl'implication "Si le terme t est typable\, alors il est normalisable"\
n(*Propriété de Terminaison*). La notion de normalisation (i.e.\ntermina
ison) admet de nombreuses variantes: on en verra deux\, la\nréduction de
tête (HN\, Head Normalization) et la réduction faible (WN\,\nWeak Normal
ization). On verra aussi que les ITS ont des conséquences en\nlambda-calc
ul qui sont *externes* à la théorie des types.\n\nEtant donné un systè
me de type Sys (que Sys soit un ITS ou un système de\ntypes simples\, d'o
rdre supérieur ou non)\, la propriété de terminaison\n(typable dans Sys
=> normalisable) est souvent difficile à établir (on\ndoit généraleme
nt recourir à un argument dit de réalisabilité\, attribué\nà Tait). C
ependant\, je présenterai le système R\, introduit par Gardner\net de de
Carvalho\, dans lequel l'opérateur d'intersection peut être vu\ncomme n
on-idempotent et la terminaison repose sur un argument très\nsimple que n
ous verrons ensemble.\n\n\n2) Présenter un article (accepté récemment
à LICS) traitant de\nlambda-calcul et de réduction infinitaires et dont
voici l'abstract:\n\nInfinitary Intersection Types as Sequences: a New Ans
wer to Klop’s Problem\n\nWe provide a type-theoretical characterization
of weakly-normalizing\nterms in an infinitary lambda-calculus. We adapt fo
r this purpose the\nstandard quantitative (with non-idempotent intersectio
ns) type\nassignment system of the lambda-calculus to our infinite calculu
s.\nOur work provides a positive answer to a semi-open question known as\n
Klop’s Problem\, namely\, finding out if there is a type system\ncharact
erizing the set of hereditary head-normalizing (HHN)\nlambda-terms. Tatsut
a showed in 2007 that HHN could not be characterized\nby a finite type sys
tem. We prove that an infinitary type system endowed\nwith a validity cond
ition called approximability can achieve it.\nAs it turns out\, approximab
ility cannot be expressed when intersection\nis represented by means of mu
ltisets. Multisets are then replaced\ncoinductively by sequences of types
indexed by integers\, thus defining a\ntype system called System S.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A playful introduction to game semantics (category-light) - Cléme
nt Jacq\, PPS team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170531T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170531T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:251
DESCRIPTION:(English abstract below)\n\nUne introduction ludique à la sé
mantique des jeux (allégée en catégories)\n\nLa sémantique des jeux es
t une branche de la théorie des modèles dont l'objectif est d'interprét
er des formules de certaines logiques sous forme de jeux à deux joueurs.
\nSon objectif initial était de lier les notions de vérité et de validi
té à des concepts de théorie des jeux tels que l'existence de stratégi
es gagnantes...\n\nAprès quelques exemples historiques\, nous nous intér
esserons 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 programmatio
n.\n\nEn guise de conclusion\, nous évoquerons l'aspect formel avec la no
tion de structure catégorielle.\n\n----\n\nA playful introduction to game
semantics (category-light)\n\nGame semantics is a branch of model theory
that aims at interpreting formulas of a given logic as two-player games. I
nitially\, it was developed to link the notions of truth and validity to g
ame-theoretic notions such as the existence of winning strategies.\n\nAfte
r an historical example\, we will look informally at a more recent case of
game semantics where the games are used to model programming languages. \
n\nAt the end\, we'll mention the formal part with the notion of categoric
al model.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Quantum algorithms and Learning With Errors- based Cryptography &
Distance Labels and Tree Skeletons - Timo Zijlstra & Emmanuel Arrighi
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170614T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170614T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:276
DESCRIPTION:Quantum algorithms and Learning With Errors- based Cryptograph
y:\n\nPost quantum cryptography is meant to replace today's standards like
RSA and Elliptic Curve Cryptography (ECC)\, since these standards are thr
eathened by quantum algorithms. The most researched post-quantum candidate
s are based on lattice problems\, and in particular the Learning with Erro
rs (LWE) problem. It is assumed that there exists no quantum algorithm tha
t solves this problem efficiently. However\, in a particular setting and u
nder some strong hypothesis\, it is very easy to solve LWE using a general
ization of the Bernstein-Vazirani quantum algorithm. We will take a look a
t possible quantum cryptanalysis on LWE-based cryptographic applications.
\n\nDistance Labels and Tree Skeletons: \n\nTo answer distance queries on
a fix known graph\, it is interesting to do\nprecalculation in order to re
duce query time. A methode is to use Hub\nLabeling. Hub Labeling works wel
l on road transport network. We will\ntake a look at this methode and intr
oduce the notion of Skeleton\nDimension which give an insight on why it wo
rks well on road network.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Semantic subtyping: an introduction - Tommaso Petrucciani\, PPS te
am
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170628T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170628T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:277
DESCRIPTION:Many type systems for programming languages include a notion o
f subtyping. Subtyping is often defined syntactically by a formal system\,
but this gets increasingly complex when union\, intersection\, and negati
on types are introduced.\n\nIn the semantic subtyping approach\, instead\,
types are interpreted as sets and subtyping is defined in terms of set co
ntainment. Then\, an algorithm is derived from the definition. While the a
lgorithm is complex\, the interpretation of types serves as a fairly simpl
e specification. This approach also ensures that union and intersection on
types behave as the corresponding operations on sets.\n\nI will give an i
ntroduction to this approach and show how to define subtyping semantically
for types including arrows\, union\, intersection\, and negation\, follow
ing [Frisch et al.\, 2008]. Then\, we will look at ongoing work on adaptin
g this approach (originally studied for call-by-value languages) to lazy s
emantics.\n\n[Frisch et al.\, 2008] A. Frisch\, G. Castagna\, and V. Benza
ken\, Semantic subtyping\, JACM\, 2008.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:New PhD student introduction session - Baptiste Louf & Victor Lanv
in\, Combinatorics and PPS teams
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170927T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170927T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:297
DESCRIPTION:This special session will introduce two new PhD students who w
ill each be giving a short talk. Here are the titles and abstracts of the
talks:\n\nCombinatorial maps : algebraic and bijective enumeration\n\nComb
inatorial maps (which are embeddings of graphs on surfaces) are well\nstud
ied objects in combinatorics\, which have applications in other\ndomains\,
such as quantum gravity. The goal is to enumerate them\n(sometimes exactl
y\, sometimes asymptotically). For this purpose\, one can\nresort to (amon
g other things) bijective or algebraic methods. The\nalgebraic method is o
ften more powerful and yields results more easily\,\nhowever bijections gi
ve a more in-depth understanding of the models.\nOften\, formulas are foun
d via powerful methods\, then people try to\nre-prove them bijectively. In
this talk\, I present what I’m focusing on\,\non the bijective side (Ca
rell-Chappy formula) and on the algebraic side\n(KP equations). If time pe
rmits\, I will explain a simple bijection I\ndiscovered during my Master
’s internship.\n\n\nGradual Set-Theoretic Types\n\nA static type system
can be an extremely powerful tool for a programmer\, \nproviding early err
or detection\, and offering strong compile-time guarantees on\nthe behavio
r of a program. However\, compared to dynamic typing\, static typing\nofte
n comes at the expense of development speed and flexibility\, as staticall
y-\ntyped code might be more difficult to adapt to changing requirements.
Gradual\ntyping is a recent and promising approach that tries to get the b
est of both\nworlds\, by allowing the programmer to finely tune the distri
bution of dynamic \nand static checking over a program.\nHowever\, this "g
radualization" is sometimes too coarse\, and an expression is\noften eithe
r fully dynamic or fully static. We argue that adding full-fledged union\n
and intersection types (a.k.a. set-theoretic types) to a gradual type syst
em\nsolves this issue by making the transition between dynamic typing and
\nstatic typing smoother.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:From Cohen's Forcing to Classical Realisability: A New Approach -
Hadrien Batmalle\, Équipe Preuves et Programmes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171011T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171011T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:298
DESCRIPTION:English abstract below\n\nDu forcing à la réalisabilité cla
ssique: une nouvelle approche\n\nLa réalisabilité classique permet d'int
erpréter des théories mathématiques classiques\, comme la théorie des
ensembles ZF\, dans divers modèles de calculs (lambda-calcul avec continu
ations\, 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 c
lassiques (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. N
ous nous intéresserons ici à une nouvelle méthode pour exporter des pro
priétés des modèles de forcing aux modèles de réalisabilité\, qui pe
rmet 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 axio
me.\n\nFrom Cohen's Forcing to Classical Realisability: A New Approach\n\n
Classical realisability is a framework for interpreting classical theories
in mathematics\, such as the ZF set theory\, in various models of computa
tion (lambda-calculus with continuations\, domains...). The goal is twofol
d: from the computer scientist's point of view\, this is a method for extr
acting computational interpretations out of classical proofs\; from the ma
thematician's\, this is a trove of new models for these classical theories
(both sides being tightly interwoven). A good deal of the research in thi
s area is focussing on the structure of these models\, arising as a genera
lisation 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 pr
operties of classical realisability models. In particular we obtain interp
retations of two incompatible theories in the same model of computation\,
which clears the path to studying the computational consequences of the pr
esence\, or lack thereof\, of some axiom.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:New PhD student introduction session - Cédric Ho Thanh & Isaac Ko
nan\, Algebra and calculus team / Combinatorics team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171025T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171025T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:299
DESCRIPTION:This special session will introduce two new PhD students who w
ill each be giving a short talk.\n\nIsaac Konan\, Bijective proof and gene
ralization of Siladic's theorem\n\nIn a recent paper\, Dousse introduced a
refinement of Siladic̀’s theorem on partitions\, by using the method o
f weighted words\, where the different parts could take 2 colours. The pro
of 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 th
e Dousse’s theorem\, moreover which could be extended on a coloring with
more than 2 colours.\n\nCédric Ho Thanh\, Opétopes\, Réécriture\, et
Koszulité\n\nMa thèse consiste en 3 mots que je vais tenter d'expliquer.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Typing Parallelism and Communication through Hypersequents - Franc
esco Antonio Genco\, Technische Universität Wien
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171108T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171108T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:322
DESCRIPTION:We present a Curry–Howard correspondence for Gödel logic ba
sed 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\, followi
ng A. Avron's 1991 thesis on the connection between hypersequents and para
llelism\, we discuss the generalisation of the employed techniques for oth
er intermediate logics.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Well Quasi-Orders and Extreme Stratospheric-Complexity-Classes of
Death --- Beaux pré-ordres et classes de complexité stratosphériques de
la mort - Simon Halfon\, ENS Cachan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171213T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171213T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:348
DESCRIPTION:It is widely known how to prove the termination of an algorith
m using well-founded orderings. It is however usually believed that no com
plexity upper bound can be derived from these termination proof\, often se
en 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 hig
h complexities. Oxygen bottles and pressure suits required\, we are going
beyond Elementary.\n\nNo special knowledge is required to follow the talk.
\n\n---\n\nNous savons tous qu’il est très pratique pour prouver la ter
minaison 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 bor
ne supérieur de complexité d’une telle preuve de terminaison. J’essa
ierai de vous donner une idée de la combinatoire compliquée que cela eng
endre\, 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.\n\nAucune connaissance spécifique n'est nécessa
ire pour suivre l'exposé.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Homotopy type theory and the fibred structure of dependent types -
Chaitanya Leena Subramaniam\, "Algebra and calculus" and "proofs and prog
rams" teams
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171115T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171115T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:349
DESCRIPTION:This is another session of the PhD introduction series.\n\nCha
itanya will do a 30 minutes talk. Given that the talk will not last as lon
g as usual\, we will also take advantage of the opportunity to discuss the
organization of the seminar.\n\nAbstract:\n\nThe talk will not be about m
y particular research problem. It will seek instead\nto give a gentle pict
orial introduction to the inherent structure \nof dependent types and how
this structure determines what dependent types and\ndependently-typed prog
rams (or proofs) *mean*.\n\nThe focus will be on why this structure natura
lly leads to homotopy type theory\nand univalence. As a bonus\, and if tim
e permits\, there will be some remarks\non univalence and extensionality.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:New PhD student introduction session. [1] From pointless topology
to formal topology [2] ACC0 and multiparty communication: fighting the log
n barrier. - Axel Osmond & Yassine Hamoudi\, [1] "Algebra and calculus" a
nd "Proofs and programs" teams\, [2] Algorithms and complexity team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171206T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171206T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:351
DESCRIPTION:[1] While point-set topology is highly practical as a framewor
k to do\nspatial reasoning\, one can rise some ontological and logical sus
picions\nabout naive notion of points as they constitute idealized objects
with\nsomewhat inaccessible aspects in a constructive and finite point of
\nview. Locales and Frames theories are two deeply entangled realms aimed\
nat rebuilding topology on latticial and categorical foundations\, in\nwhi
ch usual notions of points\, opens\, subspaces\, separability\,\ncompacity
... can be reexpressed as first order algebraic properties in\nlatticial c
ontext\, or both generalized and made constructive.\n\nFormal topology goe
s further into this last direction\, using systems of\naxioms about coveri
ngs as a deductive systems which leads to a\ntype-theoretic flavored\, pre
dicative and constructive topology\, endowed\nwith multiple and finer noti
ons of points\, separability... and suited\nfor intuitionistic reasoning.
\n\n[2] The Number On the Forehead model is a multiparty communication gam
e 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 t
he players in such a way that each player i sees all of it except xi (as i
f xi is written on the forehead of player i).\n\nA central open question i
n this model\, called the log n barrier\, is to find a function which is h
ard 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 com
plexity\, as it could help to separate ACC0 from other complexity classes.
\n\nIn this talk\, we will recall first the connection between ACC0 and co
mmunication complexity\, and then describe a new efficient communication p
rotocol that prevents some important functions from breaking the log n bar
rier.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Linear logic proof nets and Taylor expansion. - Jules Chouquet\, P
roofs and Programs team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171122T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171122T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:361
DESCRIPTION:I will first introduce linear logic proof nets\, for the multi
plicative and exponential fragment (MELL)\, and I will especially insist o
n the computational meaning of the exponential boxes: these are constructi
ons containing the possibility of duplication and deletion of entire parts
of the structures (all the non linear part of the calculus).\n\nOnce thes
e notions are introduced\, I will explain how it is possible to express th
is 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.\n\n
If we have time\, I will try to give an idea of some algebraic issues conc
erning this construction\, and a method to show for example\, that the nor
mal form of the Taylor expansion of a MELL always converges.\n\nNB: Taylor
expansion is here analogical to the lambda calculus (with its differentia
l version too) one\, if someone heard about it\, it can give a first intui
tion.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Unix filesystems and First-Order Theory of an Algebra of Feature T
rees with Updates - Nicolas Jeannerod\, Team Analysis and conception of sy
stems
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180207T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180207T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:423
DESCRIPTION:In the CoLiS project (for Correctness of Linux Scripts)\, our
mid-term\ngoal is to automatically verify certain properties on installati
on\npackages that may include shell scripts. In order to do that\, we want
\nto write a symbolic execution tool that would compute abstract\nspecific
ation for each installation script in term of filesystem\ntransformations.
\n\nWe investigate a logic of an algebra of trees with an update\noperatio
n\, which expresses that a tree is obtained from an input tree\nby replaci
ng a particular direct subtree while leaving the rest\nintact. This operat
ion improves on the expressivity of existing logics\nof tree algebras in o
ur case of feature trees. These allow for an\nunbounded number of children
of a node in a tree.\n\nWe show an efficient way of testing the satisfiab
ility of existential\nclauses in this algebra that can lead to an efficien
t implementation\nof our symbolic execution engine. We also show the decid
ability of the\nfirst-order theory of this algebra via a weak quantifier e
limination\nprocedure which is allowed to swap existential quantifiers for
\nuniversal quantifiers.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Refactoring ML programs using ornaments - Thomas Williams\, Galliu
m\, INRIA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180131T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180131T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:424
DESCRIPTION:Ornaments are a way to describe changes in datatype definition
s that preserve their recursive structure\, reorganizing\, adding\, or dro
pping some pieces of data. The relation between two types given by an orna
ment 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 prog
ram refactored to work on an ornamented datatype. \n\nIn this talk\, I wil
l explain how ornaments can be used to automatically lift a function. I wi
ll present a prototype implementation of lifting along ornaments for a sub
set of OCaml and describe some families of use cases. I will introduce a p
rincipled approach to obtaining a lifting from the base code\, as abstract
ion followed by specialization. I will explain how this approach allows us
to prove the correctness of the lifting.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:"A concise introduction to logical relations" followed by "A Logic
al Relation for Monadic Encapsulation of State" - Leo Stefanesco\, Équipe
s "Preuves et Programmes" et "Algèbre et Calcul"
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171220T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171220T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:426
DESCRIPTION:1st part (E for Everyone):\nA concise introduction to logical
relations\n\nLogical relations are a powerful technique to prove propertie
s about programs. In particular\, for proving that two programs are contex
tually equivalent.\n\nIn this talk\, we will see that\, in System F (aka t
he polymorphic lambda calculus)\, the only program of type ∀ a\, a → a
is the identity.\n\nI will also sketch how to extend logical relations to
realistic languages such as ML.\n\n\n2nd part (POPL talk rehearsal):\n\nA
Logical Relation for Monadic Encapsulation of State\n\nWe present a logic
al relations model of a higher-order functional programming language with
impredicative polymorphism\, recursive types\, and a Haskell-style ST mona
d type with runST. We use our logical relations model to show that runST p
rovides proper encapsulation of state\, by showing that effectful computat
ions encapsulated by runST are heap independent. Furthermore\, we show tha
t contextual refinements and equivalences that are expected to hold for pu
re 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.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Recent updates in quantum machine learning & Election de leader da
ns un réseau radio simple saut avec detection de collision - Alessandro L
uongo & Ny Aina Andriambolamalala\, Algorithms and complexity team & Combi
natorics team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180124T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180124T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:427
DESCRIPTION:*Recent updates in quantum machine learning*\n\nIn this talk w
e are going through some recent algorithms in the field of\nquantum machin
e learning. Most of the techniques use tools from quantum\nalgorithmics su
ch as counting\, optimizing\, estimating distances and\nsingular values wh
ich will be introduced here. Using these primitives\nit's possible to buil
d more complex operations of a matrix algebra. \nI'll also describe a clas
sical machine learning algoritm in the process\nof being translated in a f
ully fledged quantum algorithm. This is the\nfirst biologically plausible
quantum algorithm with an exponential\nspeedup w.r.t the dimension of the
space and the number of datapoints.\nThis quantum algorithm has been simul
ated and used to classify\nhandwritten digits with high accuracy.\n\n*Elec
tion de leader dans un réseau radio simple saut avec detection de collisi
on*\n\nLes résultats de Dan Willard (1986) montrent un algorithme\nrandom
izé d'élection de leader en temps moyen $O(\\log\\log{n})$.\n\nDepuis\,
la question de savoir s'il existe un algorithme\nconvergeant en temps log-
logarithmique mais avec très forte probabilité\nest ouverte.\n\nNous ré
pondons affirmativement à cette question. Nous montrons aussi\ncomment ut
iliser nos résultats pour élaborer des protocoles\nd'élection dans dive
rs modèles de systèmes distribués.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Modèles analytiques pour les performances des réseaux cellulaire
s - Narcisse Nya Kamtchoum\, LIP6
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180214T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180214T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:436
DESCRIPTION:Afin d'augmenter le débit et accroître la couverture réseau
\, les réseaux mobiles ne cessent d'évoluer rapidement vers des techno
logies caractérisées par des interfaces radio plus sophistiquées. Par
exemple\, alors que le déploiement des réseaux 4G ne faisait que commen
cer\, les premières mises à jour des solutions LTE-A étaient déjà pl
anifiées par les opérateurs et Actuellement\, les technologies 5G font
l'objet de recherches actives dans le monde entier. Ces changements rapid
es sont motivés par l'explosion du trafic mobile\, tel que prédit par d
e nombreuses études et observé dans les réseaux actuels.\n\nCependant\
, les opérateurs ont du mal à s'adapter à la proportion toujours grand
issante d'utilisateurs mobiles et à leur offrir une qualité d'expérien
ce (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 qu
alité des services offerts aux utilisateurs. Notre objectif est de propo
ser des modèles analytiques pour l'évaluation des performances des rés
eaux cellulaires en tenant compte de la mobilité des utilisateurs. Tout
en permettant de résoudre des problèmes d'évaluation de performance le
s plus complexes\, ces modèles se doivent d'être simple afin de facilit
er leur utilisation.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Species of structure: a Bridge between Differential Lambda Calculu
s and Combinatorics & Verifying Database Histories - Zeinab Galal & Ranade
ep Biswas\, Algebra and computation & Modeling and verification
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180221T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180221T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:440
DESCRIPTION:*Species of structure: a Bridge between Differential Lambda Ca
lculus and Combinatorics*\n\nSpecies 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 enume
rative combinatorics and multiple tools were developed for the resolution
of differential equations of species in this setting. Later\, Fiore presen
ted a generalized definition that both encompasses Joyal's species and con
stitutes a model of linear logic.\n\nWe will first introduce and connect t
he different viewpoints of species of structure and their series counterpa
rt (analytic and normal functors) presented by Joyal\, Girard and Hasegawa
. Next\, we will examine how the bicategory of generalized species of stru
cture forms a model of differential linear logic.\n\nAs our end goal is to
develop methods of resolution of differential equations for λ-terms\, we
will investigate the possible directions to tackle this problem.\n\n&\n\n
*Verifying Database Histories*\n\nPopular 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 weake
r consistency. So\, we have to ensure that the histories of a database are
consistent with their isolation levels.\n\nUnfortunately\, these isolatio
n levels are mostly defined as low-level operations which makes it complic
ated to reason about the behavior of the system running under those isolat
ions.\n\nIn this talk\, we will present some popular isolation levels and
consistency criteria for databases. We will introduce a framework\, in whi
ch it becomes easier to formally reason about the behavior of a system. Th
en we will explore the complexities of deciding some consistency criteria
using that framework.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Generalization of binary search in trees and other structures - Me
ngchuan Zou\, Theory and algorithmics of graphs team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180321T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180321T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:528
DESCRIPTION:The tree search problem is the following generalization of the
binary search problem. A search\nstrategy is required to locate an unknow
n target node t in a given tree T. Upon querying a node v of\nthe tree\, t
he strategy receives as a reply an indication of the connected component o
f T \\ {v}\ncontaining the target t. The cost of querying each node is giv
en by a known non-negative weight\nfunction\, and the considered objective
is to minimize the total query cost for a worst-case choice of\nthe targe
t.\n\nWe will also introduce some known facts on other structures and how
tree search problem is related to\nother problems via equivalences.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Box-Total Dual Integrality and k-Edge-Connectivity - Emiliano Lanc
ini\, Laboratoire d'Informatique de Paris Nord
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180502T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180502T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:544
DESCRIPTION:In the first half of the 20th century the distribution of elec
tricity became a major issue for many european nations. From this situatio
n arose the problem of building a connected network of minimum length.\nTh
e 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.\n\nNowadays it is often
required that telecommunication networks keep unaltered their functionalit
y even after the failure of some of their links. \nThis leads to a general
isation of the minimum spanning tree problem named k-edge-connected spanni
ng subgraph problem.\n\nIn this talk we show a characterisation of a graph
class in terms of integrality properties of polyhedra naturally associate
d to the k-edge-connected spanning subgraph problem.\n\nThe concept of tot
al dual integrality (TDI) dates back to the works of Edmonds\, Giles and P
ulleyblank in the late 70's\, and is strongly connected to min-max relatio
ns in combinatorial optimisation.\n\nThe system Ax>=b is TDI if\, in the f
ollowing equation\, for each integer vector c\, for which the minimum in t
he following equation is finite\, there exists an integer optimal solution
for the maximum.\n\nmin {cx: Ax>= b} = max {yb: yA = c\, y >= 0}\n\nWe ar
e interested in the stronger property of box-TDIness. A system Ax>=b is ca
lled *box-TDI* if the system Ax >= b\, l <= x <= u is TDI for all rational
vectors l and u.\n \nWe prove that\, for k>=2\, the k-edge-connected span
ning 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.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Translating a Concurrent Lambda Calculus into Linear Logic proof (
nets) - Yann Hamdaoui\, Proofs and Programs and Conception and Analysis of
Systems teams
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180328T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180328T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:548
DESCRIPTION:Logical translations of intuitionnistic logic into linear logi
c have been studied for their sole interest. Incidentally\, they provide t
ranslations of simply typed lambda calculus to linear logic: apart from it
s theoretical insights\, the asynchronous nature of linear logic's cut-eli
mination make it also an interesting target of compilation\, enabling dist
ributed 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.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Probabilistic Stable Functions on Discrete Cones are Power Series.
- Raphaëlle Crubillé\, Algebra and calculus\, proofs and programs teams
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180425T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180425T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:559
DESCRIPTION:The category of probabilistic coherence spaces (PCoh_!)\, intr
oduced by Danos and Ehrhard\, is a fully abstract model for PCF with *disc
rete* probabilities\, where morphisms can be seen as power series. The cat
egory Cstab_m\, of measurable cones and measurable stable functions\, has
been introduced by Ehrhard\, Pagani and Tasson as a model for PCF with *co
ntinuous* 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.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:New PhD student introduction session - Paulina Cecchi & Antoine Al
lioux\, Automata\, Combinatorics teams & Algebra and calculus\, proofs and
programs teams
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180418T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180418T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:570
DESCRIPTION:*****\nPaulina Cecchi\n\nTitle: Some interactions between word
s combinatorics and symbolic dynamics.\n\nAbstract: Word combinatorics has
been fruitfully used to study several\ntopological and mesure-theoretic p
roperties of dynamical systems\, through\nthe analysis of suitably chosen
symbolic dynamical systems. In this talk\,\nwe will introduce some notions
of symbolic dynamics and present some\nexamples which illustrate how word
combinatorics can be used as a tool to\nsolve questions arising from this
branch of mathematics.\n\n*****\n\n*****\nAntoine Allioux\n\nTitle: The c
urse of Martin-Löf identity type\n\nAbstract: The identity type of Intuit
ionistic Type Theory (ITT) endows types with a structure of infinity-group
oid. This higher structure follows from the fact that the Uniqueness of Id
entity Proof (UIP) is not derivable in ITT. \nHomotopy Type Theory (HoTT)
takes advantage of this observation by enriching ITT with new principles w
hich are coherent with this interpretation\, namely the Univalence Axiom a
nd the Higher Inductive Types (HITs).\n\nHITs are a generalization of indu
ctive types which allow\, in addition to create regular inhabitants of an
inductive type\, to postulate identities between them as well as identitie
s between these identities\, and that ad infinitum. It is then tempting to
try to present mathematical structures using these new types like one wou
ld do in mathematics using generators and relations.\n\nHowever\, problems
quickly arise as soon as one needs a strict equality. Indeed\, the identi
ty type expresses a weak equality leading to the usual coherence problems.
Trying to solve these naively\, we run into the problem of having to defi
ne an infinite sequence of coherence data.\n\nIf HoTT is to be a credible
foundation of mathematics\, the question of formalizing structures which n
eed a strict equality is crucial. The answer to this question rests\, in p
art\, upon our achievement to either present these structures differently
in the existing theory or to enrich it so that it becomes tractable to exp
ress them.\n\n*****
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:An Asynchronous Soundness Theorem for Concurrent Separation Logic
- Léo Stefanesco\, Algebra and calculus\, proofs and programs teams
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180523T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180523T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:575
DESCRIPTION:The talk will start with an introduction to (concurrent) separ
ation logic.\n\n---\n\nAbstract:\n\nConcurrent 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 whi
ch describe the operational behavior of the Code when confronted to its En
vironment\, both at the level of machine states (S) and of machine instruc
tions and locks (L). We then establish that every derivation tree π of a
judgment Γ ⊢ {P}C{Q} defines a winning and asynchronous strategy [π] w
ith respect to both asynchronous semantics [C]S and [C]L. From this\, we d
educe an asynchronous soundness theorem for CSL\, which states that the ca
nonical map L : [C]S → [C]L from the stateful semantics [C]S to the stat
eless semantics [C]L satisfies a basic fibrational property. We advocate t
hat this fibrational property provide a clean and conceptual explanation f
or the usual soundness theorem of CSL\, including the absence of data race
s.\n\n(Joint work with Paul-André Melliès)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Intermittent Locomotion in Graphs - Brieuc Guinard
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180411T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180411T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:582
DESCRIPTION:Everyone who has ever lost their keys in a busy room knows tha
t they cannot move at full speed and hope to find them \; one must slow do
wn 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. Th
is opposition between relocation and detection can even lead to an intermi
ttent behavior\, i.e. with different phases during the search.\nWe model s
uch search processes by memoryless explorations on graphs\, i.e. random wa
lks\, where you can decide at each step to query a node or not. The goal i
s to balance the time spent walking and the time spent querying.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Distributed decision - Laurent Feuilloley\, Équipes Compsys\, GAN
G et graphes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180620T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180620T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:598
DESCRIPTION:In this talk\, I will introduce the domain of distributed deci
sion\, and\nreview some of the results and insights gathered during my PhD
.\n\nThe underlying model of this study is the local model. The local mode
l\nis defined to answer questions of the following type: given a communica
tion\nnetwork\, whose nodes are machines\, and edges are communication lin
ks\, is it\npossible that the nodes solve some task X\, if they communicat
e only with the nodes that are close to them? A classic problem is colouri
ng: can a node choose a colour\, with only the knowledge of a small neighb
ourhood of the graph\, such that the colours chosen by the nodes form a pr
oper colouring of the graph? As in the centralized setting\, it is interes
ting to study decision problems\, that are yes-no questions\, and to defin
e complexity classes to classify these problems\; this is distributed deci
sion.\n\nThe complexity class we use as the equivalent of the class P in t
he\ncentralized setting\, is pretty small\, and it is then natural to look
at some form of non-determinism\, to have a chance to understand more pro
blems. In this\nmodel\, non-determinism can be thought as a piece of globa
l information that can\nbe verified locally. The theoretical motivation is
that to understand how\nlocal a problem is\, one can ask how much global
information is needed to solve\nit. The more practical motivation is that
if one can design schemes with little\nglobal information then it can help
to design more robust distributed\nalgorithms such as self-stabilizing al
gorithms. The results I will present play with different natural notions o
f non-determinism\, and how they influence the\ncomplexity classes defined
.\n\nI will spend time to carefully describe the model\, thus no prior kno
wledge is\nneeded.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Introduction to gradual typing with union and intersection types -
Victor Lanvin\, Équipes Preuves\, programmes\, et Systèmes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180627T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180627T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:599
DESCRIPTION:Since the advent of types in programming languages\, the two c
oncepts of static typing and dynamic typing have been engaged in a terribl
e battle. Simply querying "static typing vs dynamic typing" yields more th
an half a million results on Stack Overflow. \nOn the one hand\, static ty
ping provides strong safety guarantees before a program is even executed\,
by checking during compilation that types are not misused. On the other h
and\, dynamic typing is more flexible and is better suited to rapid protot
yping. With both approaches having strong arguments in their favor\, the b
attle seems endless. \nYet\, all hope is not lost. Gradual typing is a re
cent approach that aims at combining the safety guarantees of static typin
g with the flexibility and development speed of dynamic typing. The idea b
ehind it is to introduce an "unknown" type\, used to inform the compiler t
hat additional type checks may need to be performed at run time in some pl
aces. Programmers can then "gradually" add type annotations to a program\,
and control precisely how much checking is done statically versus dynamic
ally.\nOur work aims at integrating union and intersection types with grad
ual typing to allow for stronger safety guarantees and a finer control ove
r dynamic types.\n\nNote: this will (should) be a very general presentatio
n about gradual typing and set-theoretic types consisting mostly of practi
cal examples and without too many technical details. Don't hesitate to bri
ng your computer\, a book\, or your Nintendo Switch™ if you already know
the topic. :-)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Unifying non-commutative arithmetic circuit lower bounds & Robustn
ess of Programs Against Consistency Relaxation - Pierre Ohlmann & Sidi Moh
ammed Beillahi\, Équipe automate & Équipe vérification
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180606T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180606T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:600
DESCRIPTION:Unifying non-commutative arithmetic circuit lower bounds (Pier
re Ohlmann)\n\nWe develop an algebraic lower bound technique in the contex
t \nof non-commutative arithmetic circuits. To this end\, we introduce \np
olynomials for which the multiplication is also non-associative\, and\nfoc
us on their circuit complexity. We show a connection with \nmultiplicity t
ree automata\, leading to a general algebraic \ncharacterization. We use i
t to derive meta-theorems for the \nnon-commutative case\, and highlight n
umerous consequences in terms of \nlower bounds.\n\n&&\n\nRobustness of Pr
ograms Against Consistency Relaxation (Sidi Mohammed Beillahi)\n\nSequenti
al Consistency (SC) and Serializability (Ser) are the classical consistenc
y models for concurrent and distributed programs. They are the intuitive m
odels for developers. Due to the costly synchronization required by the tw
o models\, most of existing memory models and distributed implementations
of data structures do not use these two models. Instead\, in order to redu
ce 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.\nWe address in this work the pro
blem of detecting unexpected behaviors of a program that were observed whe
n weakening the consistency model. In particular\, we check whether the tw
o sets of executions traces of a program over the SC (resp\, Ser) model an
d some weaker consistency model coincide or not. We characterize the set o
f executions traces that violate this equality and drive a decision proced
ure to detect these traces. In the case where there are no traces that vio
late this equality we refer to a program to be Robust.\n\nA joint work wit
h Ahmed Bouajjani and Constantin Enea
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Denotational semantics of Linear Logic with least and greatest fix
points - Farzad Jafarrahmani
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180912T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180912T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:636
DESCRIPTION:We develop a denotational semantics of full propositional clas
sical linear logic extended with least and greatest fixpoints of formulae
(\\mu LL) in coherence spaces with totality. The presence of totality pred
icates\, which are a denotational account of the syntactic notion of norma
lization\, 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 n
umbers 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 g
eneral pattern. We also encode the exponentials of linear logic using leas
t and greatest fixpoints and then explain the difference between the new e
xponentials and the original ones from denotational semantics point of vie
w. \nThis is based on joint work by Thomas Ehrhard.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Newcomers' session - Abishek De & Simon Mauras
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181017T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181017T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:672
DESCRIPTION:Abishek De : Distributed Control Problem for Free Choice Syste
ms\n\nThe distributed synthesis problem is about constructing correct dist
ributed systems\, i.e.\, systems that satisfy a given specification. We co
nsider 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 com
municate via rendezvous (asynchronous automata). There are a few classes o
f 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.\n\n----------------------------\nSimon Mauras :
Social choice theory\, and a small survey about rank aggregation\n\nHow s
hould we vote? This question has been adressed by philosophers and mathema
ticians since the XVIIIth century\, but no satisfactory solution exists. T
he talk will start with classical results on social choice theory and move
on to the aggregation of rankings seen as an optimization problem. We wil
l discuss NP-Hardness\, Hardness of approximation and Approximation algori
thms for several variants of this problem.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:New PhD session - Anupa Sunny & Zhouningxin Wang
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181031T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181031T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:702
DESCRIPTION:Explicit\, Almost Optimal Epsilon-Biased Sets\n---------------
-----------------------------\n\nby Anupa Sunny\n\nAbstract: This talk is
based on a paper by Amnon Ta-Shma on the construction of epsilon biased se
ts which have a support size close to the Gilbert-Varshamov bound\, a noti
on from coding theory. We will look at the Rozenman-Wigderson constructio
n of the epsilon-biased set in which the bias of a set is amplified by tak
ing a walk over an expander graph. We will then look at Ta-Shma's construc
tion which is based on a modified version of the zigzag product\, namely t
he s-wide replacement product.\n\n\nHomomorphism of signed graphs\n-------
----------------------\n\nby Zhouningxin Wang\n\nAbstract: The signed grap
h is a graph whose edges are assigned with the signs + and -. A homomorphi
sm of one graph to the other preserves the adjacencies and incidences of t
hese two edges. We extend the concept of homomorphism for signed graphs. A
n intuitive example will be given to explain why we consider the homomorph
ism 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. I
n the last part\, we will show the necessary and sufficient conditions for
a signed K_4-subdivision being a core.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Writing (large) LaTeX documents with the knowledge package. - Thom
as Colcombet\, Automata team
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181114T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181114T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:715
DESCRIPTION: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 wi
ll read in order to learn the wonderful stuff you have developed at IRIF.\
n\nClearly\, there are some pitfalls to avoid. Sometimes a scientifically
excellent thesis turns out to be barely usable\, because definitions are d
ifficult 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 atten
tion 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.\n\nOne 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 subj
ect. 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 ad
vertisement for the LaTeX package « knowledge »).\n\nIf you want to test
\, you can bring your laptop with an up-to-date distribution of LaTeX.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Type theoretical approach to opetopes - Cédric Ho Thanh\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181128T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181128T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:727
DESCRIPTION:Opetopes are shapes (akin to globules\, cubes\, simplices\, et
c.) introduced to describe laws and coherence in higher categories. Their
classical definitions\, however\, makes them difficult to manipulate effic
iently. In this presentation\, I will present ongoing works aiming to desc
ribe them completely from a type-theoretic standpoint. If time permits\, I
will showcase a proof checker for opetopes.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lower bounds for arithmetic circuits via the Hankel matrix - Pierr
e Ohlmann\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190227T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190227T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:811
DESCRIPTION:We study the complexity of representing polynomials by arithme
tic circuits in both the commutative and the non-commutative settings. Our
approach goes through a precise understanding of the more restricted sett
ing where multiplication is not associative\, meaning that we distinguish
(xy)z from x(yz).\n\nOur first and main conceptual result is a characteriz
ation result: we show that the size of the smallest circuit computing a gi
ven 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
.\n\nThe study of the Hankel matrix provides a unifying approach for provi
ng lower bounds for polynomials in the (classical) associative setting. We
demonstrate this by giving alternative proofs of recent results proving s
uperpolynomial and exponential lower bounds for different classes of circu
its as corollaries of our characterization result.\n\nOur main technical c
ontribution 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) c
ommutative and non-commutative settings. In particular in the non-commutat
ive 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.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Partitions and Bijections - Isaac Konan\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190306T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190306T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:812
DESCRIPTION:"For any positive integer n\, there are as many partitions of
n into\ndistincts parts as partitions of n into odd parts". This identity
stated\nby Euler is quite trivial to prove by calculations\, but not easy
show\nbijectively.\n\nI will discuss bijections for some well-known partit
ion identities\, such\nas Schur partition identity and q-binomial coeffici
ent.\n\nNB: Open talk\, all you need is just how to count objects.
LOCATION:Salle 3014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Toward a Cubical Type Theory Univalent by Definition - Hugo Moenec
laey\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190724T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190724T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:915
DESCRIPTION:Univalent foundations are based on a geometric interpretation
of identity types in type theory. We will explain this interpretation\, th
en we will give a brief introduction to Cubical Type Theory and explain wh
y it is useful in this context. Then we will present some ideas from param
etricity and sketch how we are trying to use them to build a variant of Cu
bical Type Theory.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The PhD Seminar strikes back - (New) Phd Students
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191113T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191113T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:994
DESCRIPTION:Every new/old PhD student is invited to come and talk about he
r/his research interests.\n\nEach talk will be 2-5 minutes long\, without
any slides\, and should be understandable by everyone
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Controlling a random population - Pierre Ohlmann\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191120T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191120T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:995
DESCRIPTION:Bertrand et al. (2017) introduced a model of parameterised\nsy
stems\, where each agent is represented by a finite state system\, and\nst
udied the following control problem: for any number of agents\, does\nther
e exist a controller able to bring all agents to a target state? They\nsho
wed that the problem is decidable and EXPTIME-complete in the\nadversarial
setting\, and posed as an open problem the stochastic setting\,\nwhere th
e agent is represented by a Markov decision process. In this\npaper\, we s
how that the stochastic control problem is decidable. Our\nsolution makes
significant uses of well quasi orders\, of the max-flow min-\ncut theorem\
, and of the theory of regular cost functions.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Return of the PhD Seminar - (Old) Phd Students
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191127T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191127T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:1004
DESCRIPTION:Every new/old PhD student is invited to come and talk about he
r/his research interests.\n\nEach talk will be 2-5 minutes long\, and shou
ld be understandable by everyone.
LOCATION:Salle 3052
END:VEVENT
END:VCALENDAR