BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Google Inc//Google Calendar 70.9054//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
DESCRIPTION:Sémantique seminar of IRIF
NAME:Sémantique
REFRESH-INTERVAL:PT4H
TIMEZONE-ID:Europe/Paris
X-WR-CALDESC:Sémantique seminar of IRIF
X-WR-CALNAME:Sémantique
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:Interpreting infinite terms - Andrew Polonsky\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160329T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160329T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:38
DESCRIPTION:Most standard models of the lambda calculus validate the princ
iples of\ninfinitary rewriting (which include identification of meaningles
s terms).\nFor example\, in Scott models\, the interpretation of every fix
ed point\ncombinator is equal to the limit (in the model) of interpretatio
ns of\n\n\\f.f(Ω)\, \\f.f^2(Ω)\, \\f.f^3(Ω)\, ...\, \\f.f^n(Ω)\, ....\
n\nThe infinite term \\f.f(f(f...)) is the limit of the above sequence\, a
nd in\nthe infinitary lambda calculus all fpcs reduce to this term\, which
is an\ninfinitary normal form.\nIt would seem natural to extend the inter
pretation function to cover\ninfinitary terms as well\, however\, naive at
tempts to do this fail.\nThe problem is already present in the first-order
case: finite terms over\na signature ∑ can be interpreted by means of t
he initial semantics -- where\nthe free algebra of terms admits a canonica
l homomorphism to any other\n∑-algebra.\nHowever\, the infinite terms ar
e elements of the cofinal coalgebra\, which\nuniversal property concerns m
aps INTO the algebra\, rather than out of it.\nWe are thus faced with a "k
oan":\n\n *What does it mean to interpret infinite terms?*\n\nWhile we
shall not provide a (co)final solution to this koan\, we will offer\ngerm
s of some possible approaches\, with the hope of starting a discussion\nth
at could follow this short talk.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Syntax directed coproofs for Propositional Dynamic Logic - Daniel
Leivant\, Indiana University Bloomington
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160517T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160517T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:44
DESCRIPTION:Propositional dynamic logic (PDL) is at the core of\nreasoning
about dynamic systems. We present a syntax directed\nformalism for PDL\,
built on coproofs.\n\nContrary to proofs\, which are generated inductivel
y top-down\,\ncoproofs are generated coinductively bottom-up\, and may hav
e infinite branches.\nHowever\, our inference rules allow this only via st
ate-changes\,\nand as a result are sound.\n\nWe also prove the semantic co
mpleteness of our formalism\, and apply it\nto obtain new interpolation th
eorems for PDL.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:L'encodage probabiliste: vers une formalisation systématique des
langages probabilistes\, déterministiques et potentiellement divergents.
- Flavien Breuvart\, INRIA Focus (Université de Bologna\, IT)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160407T160000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160407T170000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:50
DESCRIPTION:Il existe deux formalisations des langages/systèmes probabili
stes: l'une est de considérer l'arbre des dérivations (avec branchements
probabilistes)\, l'autre est de considérer des distributions de probabil
ités. Avoir accès à l'arbre de dérivation est pratique pour les preuve
s car on a accès à l'historique complet\, mais lorsque l'arbre est infin
i\, le formalisme est très lourd et peu explicite. La formulation à base
de distributions est plus simple et donne des théorèmes élégants mais
engendre des preuves très complexes (où il faut souvent retrouver l'his
torique du calcul).\nDans cet exposé nous verrons qu'il est possible de r
écupérer le meilleur des deux mondes grâce à un théorème d'encodage
probabilistique inspiré de la théorie catégorique des coalgèbres. Nous
verrons qu'il s'agit d'un outil systématique qui\, à l'instar de l'indu
ction ou la coinduction\, permet de structurer des preuves et des définit
ions complexes. Pour des raisons de temps\, nous n'évoquerons que briève
ment comment ce schéma de preuve nous permet de redéfinir une version pr
obabiliste de notions usuelles telles que les types intersection probabili
stes ou les candidats de réductibilité probabilistes.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Probabilistic lambda-theories - Thomas Leventis\, I2M Marseille
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160607T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160607T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:73
DESCRIPTION:In the usual deterministic lambda-calculus the confluence of t
he unique computation rule\, the beta-reduction\, makes it easy to turn th
e reduction into an equality\, the beta-equivalence. This idea to consider
not computation but equalities on terms gives rise to the notion of lambd
a-theory. On the other hand the probabilistic lambda-calculus is usually t
reated only in terms of computation. In particular we know that we must im
pose a reduction strategy for the probabilistic choice if we want the calc
ulus to make sense.\n\nIn this talk we will recover this notion of present
ation through equalities in the probabilistic lambda-calculus. We will sho
w how some usual notions can be translated in the probabilistic world. In
particular we will define a notion of probabilistic Böhm tree\, and show
a separability result. This will implies that just like in the determinist
ic setting the Böhm tree equality is the same as the observational equiva
lence.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Empirical Models and Contextuality - Shane Mansfield\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160705T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160705T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:81
DESCRIPTION:I will begin by presenting a structural description of the kin
d of\nempirical data which arises in physical experiments\, using the\nlan
guage of sheaf-theory. A potential feature of such data is\ncontextuality
(including as a special case non-locality) which can be\nneatly characteri
sed in this setting. The feature does not arise in\nclassical data\, and a
number of recent results indicate that it is the\nkey feature in enabling
quantum advantages or speedups over classical\nbehaviour in a variety of
computational scenarios. The sheaf-theoretic\nperspective exposes a qualit
ative hierarchy of strengths of\ncontextuality and I will also mention rec
ent efforts to quantify\ncontextuality via linear programming. Finally I w
ill report on work in\nprogress on developing a resource theory for contex
tuality\, beginning\nwith an algebra of empirical models under whose opera
tions\ncontextuality is monotonically decreasing.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Krivine machine and Taylor expansion in a non-uniform setting - An
toine Allioux\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160607T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160607T110000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:83
DESCRIPTION:The Krivine machine is an abstract machine implementing the li
near head reduction of $\\lambda$-calculus. Ehrhard and Regnier gave a res
ource sensitive version returning the annotated form of a $\\lambda$-term
accounting for the resources used by the linear head reduction. These anno
tations take the form of terms in the resource $\\lambda$-calculus.\n\nWe
generalize this resource-driven Krivine machine to the case of the algebra
ic $\\lambda$-calculus. The latter is an extension of the pure $\\lambda$-
calculus allowing for the linear combination of $\\lambda$-terms with coef
ficients taken from a semiring. Our machine associates a $\\lambda$-term $
M$ and a resource annotation $t$ with a scalar $\\alpha$ in the semiring d
escribing some quantitative properties of the linear head reduction of $M$
.\n\nIn the particular case of non-negative real numbers and of algebraic
terms $M$ representing probability distributions\, the coefficient $\\alph
a$ gives the probability that the linear head reduction actually uses exac
tly the resources annotated by $t$. In the general case\, we prove that th
e coefficient $\\alpha$ can be recovered from the coefficient of $t$ in th
e Taylor expansion of $M$ and from the normal form of $t$.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Finite Family Developments for the Linear Substitution Calculus -
Pablo Barenbaum\, Université de Buenos Aires - CONICET
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161018T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161018T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:127
DESCRIPTION:We prove a finite family developments theorem (FFD) for the ca
lculus\nwith explicit substitutions Linear Substitution Calculus (LSC). Th
e\nnotion of redex family is obtained by adapting Lévy labels to\nsupport
the two distinctive features of LSC\, namely its use of\ncontext rules th
at allow substitutions to act "at a distance" and\nalso the set of equatio
ns modulo which it rewrites. We then apply FFD to\nprove a number of resu
lts for LSC including: an optimal reduction result\,\nan algorithm for sta
ndardisation by selection\, and normalisation of a\nlinear call-by-need re
duction strategy.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Traced star-autonomous categories are compact closed - Masahito Ha
segawa\, Research Institute in Mathematical Sciences (RIMS)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161018T113000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161018T123000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:128
DESCRIPTION:For years we have been bothered by a small mistery on categori
cal models\nof Linear Logic (star-autonomous categories) and Geometry of I
nteraction\n(compact closed categories\, typically arising from traced mon
oidal categories\nvia Int-construction): is there a proper intermediate st
ructure between\nstar-autonomous categories and compact closed categories\
, that is\, a traced\nstar-autonomous category which is not compact closed
?\nWe settle this issue by showing that any traced star-autonomous categor
y is\nactually compact closed.\n\nWe also discuss what would happen if we
remove symmetry\, thus the following\nquestion: is there a non-symmetric s
tar-autonomous category with a (suitably\ngeneralized) trace which is not
pivotal? Our recent attempt suggests that\nthe answer is again no\, but th
e situation is much subtler than the symmetric\ncase.\n\nThe result on the
symmetric case is a joint work with Tamas Hajgato.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Safe and Scalable Cloud Programming - Gustavo Petri\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161108T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161108T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:135
DESCRIPTION:I will present AEON (Atomic Events and Ownership Networks)\, a
programming model for safe and scalable cloud computing. AEON is based o
n the well-known paradigms of object-orientation and event-driven programm
ing. AEON’s runtime system guarantees a linearizable and deadlock-free s
emantics for events that span across multiple objects and servers. Moreove
r\, to achieve an economical and scalable solution\, our runtime system pr
ovides seamless elasticity (the capability to adapt the resources usage to
the actual workload)\, and exploits the object graph — the ownership ne
twork — to enhance parallelism. In this talk will concentrate on the saf
ety aspects of the semantics of AEON\, and show some experimental scalabil
ity results.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Call-by-name\, call-by-value and intuitionistic logic - José Esp
írito Santo\, University of Minho
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161115T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161115T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:140
DESCRIPTION:Call-by name (CBN) and call-by-value (CBV) have been defined a
s the dual solutions to a critical pair at the heart of cut-elimination in
classical sequent calculus. When one moves to intuitionistic logic\, this
symmetric picture breaks\, but what happens precisely? How are such defin
itions adapted to the intuitionistic case? How do the resulting calculi re
late to the many other proposals for intuitionistic CBV and CBN calculi? A
nd what does that break of duality say about intuitionistic logic? We find
that proof-theory alone distills new CBV and CBN lambda-calculi which agr
ee\, in a technical sense\, with the computational lambda-calculus and the
ordinary lambda-calculus\, respectively\; but the former distilled calcul
us is contained in the latter - a vindication of Plotkin. This containment
\, in turn\, rests on another asymmetry: a certain permutative/focalizatio
n conversion\, named T\, solves what remains of the classical critical pai
r in favor of CBN\, while the symmetric solution with a certain CBV conver
sion Q does not exist. In this sense we may say intuitionistic logic enjoy
s a CBN bias. Full answers to the above questions require us to work simul
taneously with sequent calculus and its equivalent bidirectional natural d
eduction. The former syntax is our starting point\, where we track the (lo
st) symmetries and find the idea of permutative conversions\; the latter s
yntax is the bridge towards more traditional programming notations. For in
stance\, only in bidirectional natural deduction one sees that T eliminate
s the difference between "let" and explicit substitution\, and only there
one understands what calling paradigm corresponds to the superimposition o
f CBN and CBV.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formal language theory beyond trees and forests - Tobias Heindel\,
Université de Leipzig
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171107T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171107T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:151
DESCRIPTION:The talk presents the theorems of Myhill-Nerode and Chomsky-Sc
hützenberger using rewriting diagrams of semi-Thue systems as paradigm ex
ample of planar acyclic circuit diagrams (PLACIDs)---the “graphical synt
ax” of monoidal categories. The talk will focus on the proposal of a de
finition of recognizable language in a monoidal category\, namely sets of
arrows that coincide with the inverse image of their direct image under a
monoidal functor to a finite monoidal category. For the case of PLACIDs\,
this class of languages is shown to coincide with the languages of automat
a in the sense of Bossut\, under modest assumptions on gates of circuit di
agrams\; moreover\, the usual notion of recognizable tree language is reco
vered. The talk presents the Myhill-Nerode theorem as a tool for solving
Bossut's open problem of automata complementation. The remainder of the ta
lk describes work in progress and future work\, in particular the Chomsky-
Schützenberger theorem for PLACIDs.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Explaining Program Differences Using Oracles - Yann Régis-Gianas\
, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161206T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161206T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:153
DESCRIPTION:Program differences are pervasive in software development\, bu
t most of the\ntime they are represented as textual differences with no re
gards to the\nsyntactic nature of programming languages or their semantics
. Thus\, they may\nbe hard to read and often fail to convey insight on the
changes on\nsemantics. Furthermore\, such low-level\, unstructured presen
tations are hard to\nreason about.\n\nWe present a formal framework to cha
racterize differences between\ndeterministic programs in terms of their sm
all-step semantics. This\nlanguage-agnostic framework defines the notion o
f /difference languages/ in\nwhich /oracles/—programs that relate small-
step executions of pairs of program\nwritten in a same language—can be w
ritten\, reasoned about and composed.\n\nWe illustrate this framework by i
nstantiating it on a toy imperative language\nand by presenting several /d
ifference languages/ ranging from trivial\nequivalence-preserving syntacti
c transformations to characterized semantic\ndifferences. Through those ex
amples\, we will present the basis of our\nframework\, show how to use it
to relate syntactic changes with their effect on\nsemantics\, how one can
abstract away from the small-step semantics\npresentation\, and discuss th
e composability of oracles.\n\nThis is joint work with Thibaut Girka (IRIF
- MERCE) and David Mentré (MERCE)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The atomic lambda-mu-calculus - Fanny He\, Université de Bath\, U
K
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170110T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170110T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:165
DESCRIPTION:The lambda-calculus studies the dynamics of computation\, but
the complexity of one computation path cannot be forecast\, neither in tim
e nor in space\, and there is no direct control on the execution environme
nt.\n\nOne approach for the former is to gain more control over duplicatio
n and deletion of terms\, by introducing sharings of common subterms insid
e a lambda-term\, similarly to optimal reduction graphs. This has been don
e by Gundersen\, Heijltjes and Parigot\, via the atomic lambda-calculus\,
a calculus extending the lambda-calculus with explicit sharings\, and allo
wing duplications on individual constructors. It enjoys full-laziness\, av
oiding unnecessary duplications of constant expressions. \n\nFor the latte
r\, an extension of the lambda-calculus linking classical formulas to cont
rol flow constructs via Curry-Howard correspondence\, the lambda-mu-calcul
us\, was developed by Parigot. New operators in the lambda-mu-calculus cor
respond to continuations\, representing the remaining work in a program. \
n\nCan we combine sharing with control operators and thus obtain another e
xtension of the lambda-calculus satisfying full-laziness and featuring con
trol operators? A first challenge is to combine explicit sharings or subst
itutions with mu-reduction and substitution\, and we introduce a right-ass
ociative application as in Saurin-Gaboardi's lambda-mu-calculus with strea
ms to overcome this challenge. \nAnother difficulty is to adapt the type s
ystem for lambda-mu with multiple conclusions\, distinguishing one main co
nclusion (with a meta-disjunction connective)\, to a type system in which
each rule can be applied to atoms (which corresponds to duplications on in
dividual term constructors)\, and where no distinction is made between obj
ect and meta-level. I will present how to combine these two type systems i
n the simplest possible way.\n\nI will present the atomic lambda-mu-calcul
us\, which aims to naturally extend the two calculi presented above\, givi
ng the simplest type system combining and preserving their properties.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Que savent les tresses sur les tableaux de Young ? - Victoria Lebe
d\, Trinity College\, Dublin
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161221T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161221T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:169
DESCRIPTION:Les tableaux de Young portent une multiplication associative\,
décrite\npar l'algorithme de Schensted. Le monoïde ainsi obtenu est app
elé\nplaxique. Il joue un rôle fondamental dans de nombreuses applicatio
ns\ncombinatoires et algébriques. On montrera que cette multiplication su
r\nles tableaux est entièrement déterminée par un tressage sur l'ensemb
le\n(bien plus simple !) des colonnes. Ici un tressage est une solution\ne
nsembliste de l'équation de Yang-Baxter. Notre tressage s'inscrit\négale
ment dans le cadre de la réécriture. Comme application\, on\nidentifiera
la cohomologie de Hochschild du monoïde plaxique\, qui\nrésiste à tout
es les approches classiques\, à la cohomologie tressée\ndes tableaux-col
onnes\, beaucoup plus accessible. Toutes les notions et\nconstructions ser
ont rappelées.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Séquences justifiées et diagrammes de cordes : deux approches de
la sémantique de jeux concurrents - Clovis Eberhart\, LAMA\, Chambéry
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161220T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161220T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:170
DESCRIPTION:Plusieurs modèles de sémantique de jeux concurrents ont éme
rgé ces\ndernières années. Dans ce travail\, on se concentre sur certai
nes de ces\napproches\, qui ont donné des modèles de CCS\, du pi-calcul
et du\nlambda-calcul non-déterministe. Un point commun informel mais sail
lant\nentre ces approches est que les stratégies innocentes sont définie
s\ncommes les faisceaux pour la topologie de Grothendieck où les parties\
nsont recouvertes par leurs vues. On propose ici de tisser un lien formel\
nentre deux de ces approches au niveau des parties et des stratégies.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Retrofitting linear types - Arnaud Spiwack\, Tweag I/O
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170124T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170124T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:182
DESCRIPTION:Type systems based on linear logic and their friends have prov
ed that they are both capable of expressing a wealth of interesting abstra
ctions. Among these the ability to mix garbage-collected and explicitly ma
naged data in the same language. This is of prime interest for distributed
computations that need to reduce latency induced by GC pauses: a smaller
GC heap is a happier GC heap.\n\nI had always had the belief that to add l
inear types to a language was a rather intrusive procedure and that a lang
uage with linear types would basically be an entirely new language. The Ru
st language is a case in point: it has a linear-like type system\, but it'
s a very different language from your run-of-the-mill functional language.
\n\nThis turns out not to be the case: this talk presents a way to extend
a functional programming language. We are targeting Haskell but there is l
ittle specific to Haskell in this presentation. I will focus mostly on the
type system and how it can be generalised: among other things the type sy
stem extends to dependent types.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Interaction morphisms - Tarmo Uustalu\, Tallinn University of Tech
nology
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170113T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170113T150000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:184
DESCRIPTION:Interaction morphisms\n\nTarmo Uustalu\, Tallinn U of Technolo
gy\n\nI will propose interaction morphisms as a means to specify how an ef
fectful computation is to be run\, provided a state in a context. An inter
action morphism of a monad T and a comonad D is a family of maps T X x D Y
-> X x Y natural in X and Y and subject to some equations. Interaction mo
rphisms turn out to be a natural concept with a number of neat properties.
In particular\, interaction morphisms are the same as monoids in a certai
n monoidal category\; interaction morphisms of T and D are in a bijective
correspondence with carrier-preserving functors between the categories of
coalgebras of D and stateful runners of T (monad morphisms from T to state
monads)\; they are also in a bijective correspondence with monad morphism
s from T to a monad induced in a certain way by D.\n\nThis is joint work w
ith Shin-ya Katsumata (University of Kyoto).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Strongly Connected Components in graphs\, formal proof of Tarjan19
72 algorithm - Ran Chen\, Inria
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170228T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170228T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:203
DESCRIPTION:There is a growing interest in programs proofs checked by comp
uter. Proofs about programs are often very long and have to face a huge am
ount of cases due to the multiplicity of programs variables and the precis
e details of the programs. This is very frustrating since we would like to
explain the proofs of correctness and publish them in scientific articles
. However if one considers simple algorithms\, we would expect to explain
their proofs of correctness in the same way as we explain a mathematical p
roof for a non too complex theorem. \n\nWe present a human readable and ra
ther intuitive formal proof for the classical Tarjan-1972 algorithms for
finding strongly connected components in directed graphs. Tarjan’s algor
ithm consists in an efficient one-pass depth-first search traversal in gra
phs which traces the bases of strongly connected components. We describe t
he algorithm in a functional programming style with abstract values for ve
rtices in graphs\, with functions between vertices and their successors\,
and with data types such that lists (for representing immutable stacks) an
d sets. We use the Why3 system and the Why3-logic to express these proofs
and fully check them by computer.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A uniform framework for substructural logics with modalities - Ela
ine Pimentel\, Universidade Federal do Rio Grande do Norte (Brasil)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170613T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170613T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:268
DESCRIPTION:It is well known that context dependent logical rules can be p
roblematic both to implement and reason about. This is one of the factors
driving the quest for better behaved\, i.e.\, local\, logical systems.\nIn
this talk we will present such a local system for linear logic (LL) based
on linear nested sequents (LNS). Relying on that system\, we propose a ge
neral framework for modularly describing systems combining\, coherently\,
substructural behaviors inherited from \\LL with simply dependent multimod
alities. \nThis class of systems includes linear\, elementary\, affine\, b
ounded and subexponential linear logics and extensions of multiplicative
additive linear logic (MALL) with normal modalities\, as well as general c
ombinations of them. The resulting LNS systems can be adequately encoded i
nto (plain) linear logic\, supporting the idea that LL is\, in fact\, a ``
universal framework'' for the specification of logical systems. \nFrom the
theoretical point of view\, we give a uniform presentation of LL featurin
g different axioms for its modal operators. From the practical point of v
iew\, our results lead to a generic way of constructing theorem provers fo
r different logics\, all of them based on the same grounds.\nThis opens th
e possibility of using the same logical framework for reasoning about all
such logical systems. \n\nThis is a joint work with Carlos Olarte and Bjö
rn Lellmann
LOCATION:Salle 2012
END:VEVENT
BEGIN:VEVENT
SUMMARY:Partiality and container monads - Niccolò Veltri\, Laboratory of
Software Science\, Tallinn
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170630T163000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170630T173000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:284
DESCRIPTION:We investigate monads of partiality in Martin-Löf type theory
\,\nfollowing Moggi’s general monad-based method for modelling\neffectfu
l computations. These monads are often called lifting\nmonads and appear i
n category theory with different but related\ndefinitions.\nIn this talk\,
we unveil the relation between containers and\nlifting monads. We show th
at the lifting monads usually employed\nin type theory can be specified in
terms of containers. Moreover\,\nwe give a precise characterization of co
ntainers whose\ninterpretations carry a lifting monad structure. We show t
hat\nthese conditions are tightly connected with Rosolini’s notion of\nd
ominance. We provide several examples\, putting particular\nemphasis on Ca
pretta’s delay monad and its quotiented variant\,\nthe non-termination m
onad.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Some bridges between lambda calculus and graphs on surfaces - Noam
Zeilberger\, University of Birmingham
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170718T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170718T150000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:289
DESCRIPTION:It turns out that enumeration of graphs embedded on surfaces (
an\nactive area of combinatorics since Bill Tutte's pioneering work in the
\n1960s) has a variety of surprising links to the combinatorics of\nlambda
calculus. In the talk\, I will give a brief survey of these\nenumerative
connections\, then focus on the 1-to-1 correspondence\n(originally describ
ed in work by Bodini\, Gardy\, and Jacquot) between\nlinear lambda terms a
nd rooted trivalent maps. The key to\nunderstanding this bijection will be
combining an interpretation of\nlambda terms as string diagrams with a Tu
tte-style decomposition of\nrooted trivalent maps with boundary. Finally\,
if time permits\, I will\ndiscuss a suggestive analogy between typing and
edge-coloring\, and use\nthis to motivate a deeper study of the surprisin
gly subtle typing\nproperties of linear lambda terms.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Frobenius spheres - Zoran Petric\, Mathematical Institute\, Academ
y of Sciences\, Belgrade
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170831T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170831T150000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:290
DESCRIPTION:Following the pattern of the Frobenius structure usually assig
ned\nto the 1-dimensional sphere\, we investigate the Frobenius\nstructure
s of spheres in all other dimensions. Starting from\ndimension $d=1$\, all
the spheres are commutative Frobenius objects\nin categories whose arrows
are ${(d+1)}$-dimensional cobordisms.\nWith respect to the language of Fr
obenius objects\, there is no\ndistinction between these spheres---they ar
e all free of\nadditional equations formulated in this language. The\ncorr
esponding structure makes out of the 0-dimensional sphere not\na commutati
ve but a symmetric Frobenius object.\n\nThe talk is based on the paper "Sp
heres as Frobenius objects"\,\nco-authored with Djordje Baralic and Sonja
Telebakovic\, which is available\nat arxiv.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Combinatorial Hopf algebras and rewriting: the rule algebra framew
ork - Nicolas Behr\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171031T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171031T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:325
DESCRIPTION:Contrary to traditional formulations of rewriting\, which tend
to rely on ideas such as category-theoretic double pushout constructions\
, the novel rule algebra framework is based upon the idea of interpreting
rewriting rules as generators of certain diagrammatic algebras. In this wh
iteboard talk\, I will present the core mathematical ideas and results\, i
ncluding the deep link between certain types of combinatorial Hopf algebra
s and rewriting theories. Some illustrative examples for the cases of disc
rete and graph rewriting will be provided.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Compositionality in Network Theory - John Baez\, UCLA Riverside
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171121T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171121T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:337
DESCRIPTION:To describe systems composed of interacting parts\, scientists
and engineers draw diagrams of networks: flow charts\, Petri nets\, elect
rical circuit diagrams\, signal-flow graphs\, chemical reaction networks\,
Feynman diagrams and the like. In principle all these different diagrams
fit into a common framework: the mathematics of symmetric monoidal categor
ies. This has been known for some time. However\, the details are more cha
llenging\, and ultimately more rewarding\, than this basic insight. Two co
mplementary approaches are presentations of symmetric monoidal categories
using generators and relations (which are more algebraic in flavor) and de
corated cospan categories (which are more geometrical). In this talk we fo
cus on the latter.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:n-Fold models of weak n-categories - Simona Paoli\, University of
Leicester
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171129T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171129T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:338
DESCRIPTION:n-fold categories are obtained by n-iterations of the internal
category construction\, starting from the category Cat. N-Fold categories
satisfying the globularity condition correspond to strict n-categories. O
ne can ask if there is an intermediate structure between n-fold categories
and strict n-categories which is a model of weak n-categories. We answer
this question positively with the introduction of the category of weakly g
lobular n-fold categories. This category is based on a new paradigm to wea
ken higher categorical structures\, and offers several advantages in terms
of applications. We will illustrate how this model is part of a wider cla
ss of Segal-type models\, and its equivalence with the Tamsamani-Simpson m
odel of weak n-categories.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:F* : Dijkstra-monads at work - Kenji Maillard\, INRIA et ENS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171205T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171205T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:411
DESCRIPTION:F* is a programming language providing proof-assistant feature
s such as\ndependent types\, a rich logic with universes and tactics. Its
primary goal is to\nimplement security critical program e.g. cryptographic
primitives (HACL*) or\nprotocols (HTTPS in MiTLS)\, prove gradually their
correction and extract to\nperformant effectful low-level code. In order
to achieve gradual proof of\neffectful code\, F* relies on weakest-precond
ition indexed monads called Dijkstra\nmonads. In this presentation we will
explain why and how Dijkstra monads are\nused in F*\, as well as how they
are often derived from usual presentations of\nmonads as can be found in
more mainstream language such as Haskell.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Intersection Types\, Linear Approximations and the Grothendieck co
nstruction - Luc Pellissier\, ENS Lyon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180117T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180117T110000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:434
DESCRIPTION:Intersection Types are a well-known family of tools that chara
cterise different notions of normalisation. We develop a general framework
for building such systems from a notion of approximation\, that allows to
recover many well-known intersection type systems\, as well as new system
s\, for every calculus that can be translated into linear logic.\nThis con
struction uses in a crucial way Melliès and Zeilberger’s “type system
s as functors” viewpoint\, as well as an adapted Grothendieck constructi
on.\n\nBased on a joint work with Damiano Mazza and Pierre Vial.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A unified framework for notions of algebraic theory - Soichiro Fuj
ii\, National Institute of Informatics (NII\, Tokyo)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180117T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180117T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:435
DESCRIPTION:Universal algebra uniformly captures various algebraic structu
res\, by expressing them as equational theories or (abstract) clones. The
ubiquity of algebraic structures in mathematics has also given rise to sev
eral variants of universal algebra\, such as symmetric and non-symmetric o
perads\, clubs\, and monads. In this talk\, I will present a unified frame
work for these cousins of universal algebra\, or notions of algebraic theo
ry. \n\nFirst I will explain how each notion of algebraic theory can be id
entified with a certain monoidal category\, in such a way that theories co
rrespond to monoids. Then I will introduce a categorical structure underly
ing the definition of models of theories. In specific examples\, it often
arises in the form of oplax action or enrichment. Finally I will uniformly
characterize categories of models for various notions of algebraic theory
\, by a double-categorical universal property in the pseudo-double categor
y of profunctors.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Codensity liftings of monads - Shin-Ya Katsumata\, National Instit
ute of Informatics\, Tokyo
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180220T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180220T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:533
DESCRIPTION:I will introduce a method to lift monads on the base category
of\na fibration to its total category using codensity monads. This\nmethod
\, called codensity lifting\, is applicable to various\nfibrations which w
ere not supported by the speaker's previous\nmethod called categorical TT-
lifting. After introducing the\ncodensity lifting\, we illustrate some exa
mples of codensity\nliftings of monads along the fibrations from the categ
ory of\npreorders\, topological spaces and extended psuedometric spaces. I
\nwill also talk about the liftings of algebraic operations to the\ncodens
ity-lifted monads. If time permits\, I will mention a\ncharacterisation o
f the class of liftings (along posetal\nfibrations with fibred small limit
s) as a limit of a certain\nlarge diagram.\n\n(Joint work with Tetsuya Sat
o\; presented in CALCO 2015)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nested and labelled sequent calculi for bi-intuitionistic proposit
ional logic - Tarmo Uustalu\, Reykjavik University and Tallinn University
of Technology
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180515T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180515T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:586
DESCRIPTION:Rauszer's bi-intuitionistic propositional logic (BiInt) is the
\nconservative extension of intuitionistic propositional logic (Int)\nwith
a connective dual to implication usually called 'exclusion'. A\n*standard
-style* sequent calculus for BiInt is easily obtained by\nextending the mu
ltiple-conclusion sequent calculus of Int with\nexclusion rules dual to th
e implication rules. However\, similarly to\nstandard-style sequent calcul
i for modal logics like S5\, this calculus\nis incomplete without the cut
rule. Cut-freeness is achievable for\nsequent calculi with non-standard se
quent forms. The *nested* and\n*labelled* calculi (Goré\, Postniece\; Pin
to\, Uustalu) were motivated by\nquite different intuitive considerations.
Yet they turn out to be very\nclose on the technical level: slightly adju
sted towards each other\,\nthey can be made isomorphic.\n\nThis is joint w
ork with Luís Pinto (Universidade do Minho).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Template games: a model of differential linear logic - Paul-André
Mellies\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180918T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180918T110000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:643
DESCRIPTION:Game semantics is the art of interpreting formulas (types) as
games and proofs (programs) as strategies interacting in space and time wi
th their environment. In order to reflect the interactive behaviour of pro
grams\, strategies are required to follow specific scheduling policies. Ty
pically\, in the case of a purely sequential programming language\, the pr
ogram (Player) and its environment (Opponent) play one after the other\, i
n a strictly alternating way. In the case of a concurrent language\, on th
e other hand\, Player and Opponent are allowed to play several moves in a
row\, in a non alternating way. In the two cases\, the scheduling policy i
s designed very carefully in order to ensure that the strategies synchroni
se properly and compose well when plugged together. A longstanding concept
ual problem has been to understand when and why a given scheduling policy
works and is compositional in that sense. In this talk\, I will introduce
the notion of template game and exhibit a number of simple and fundamental
combinatorial properties which ensure that a given scheduling policy defi
nes a monoidal closed bicategory of games\, strategies and simulations. Th
e notion of template game will be illustrated by constructing two game mod
els of linear logic with different flavors (alternating and non alternatin
g) using the same categorical combinatorics\, performed in the category of
small categories.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Differential Categories Revisited - Jean-Simon Lemay\, University
of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180918T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180918T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:644
DESCRIPTION:Differential categories were introduce to provide a minimal ca
tegorical semantics for differential linear logic. However\, there exists
three approaches to axiomatizing the derivative by deriving transformation
s\, coderelictions\, and creation maps - long thought to be distinct notio
ns. Recently\, Blute\, Cockett\, Seely and myself have revisited the axiom
s of a differential category and showed that for categorical models of dif
ferential linear logic the three approaches are equivalent. Thus\, there i
s only one notion of differentiation.\n\nLes catégories différentielles
ont été introduites afin de fournir une sémantique catégorique minime
pour la logique linéaire différentielle. Cependant\, il existe trois app
roches d'axiomatiser la dérivée par les "deriving transformations"\, "co
derelictions"\, "creation maps" - considérés pendant longtemps comme des
notions distinctes. Récemment\, avec Blute\, Cockett et Seely\, nous avo
ns revisité les axiomes d’une catégorie différentielle et démontré
que pour les modèles catégoriques de logique linéaire différentielle\,
les trois approches sont équivalentes. Il y a donc qu’une seule notion
de différentielle.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Une remarque sur les espaces cohérents probabilistes et la distan
ce opérationnelle entre les programmes - Thomas Ehrhard\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181016T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181016T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:674
DESCRIPTION:On utilise les régularités des morphismes de la catégorie c
artésienne fermée des espaces cohérents probabilistes pour majorer une
distance naturelle sur les (classes d'équivalence observationnelle) de te
rmes de PCF probabilistes par une distance définissable dans le modèle.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Finiteness spaces and generalized power series - Rick Blute\, Univ
ersity of Ottawa
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181106T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181106T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:698
DESCRIPTION:We consider Ribenboim’s construction of rings of generalized
power series. Ribenboim’s construction makes use of a special class of
partially ordered monoids and a special class of their subsets. While the
restrictions he imposes might seem conceptually unclear\, we demonstrate t
hat they are precisely the appropriate conditions to represent such monoid
s as internal monoids in an appropriate category of Ehrhard’s finiteness
spaces. Ehrhard introduced finiteness spaces as the objects of a categori
cal model of classical linear logic\, where a set is equipped with a class
of subsets to be thought of as finitary. Morphisms are relations preservi
ng the finitary structure. \n\nIn the present work\, we take morphisms to
be partial functions preserving the finitary structure rather than relatio
ns. The resulting category is symmetric monoidal closed\, complete and coc
omplete. Any pair of an internal monoid in this category and a ring induce
s a ring of generalized power series by an extension of the Ribenboim cons
truction based on Ehrhard’s notion of linearization of a finiteness spac
e. We thus further generalize Ribenboim’s constructions. We give several
examples of rings which arise from this construction\, including the ring
of Puiseux series and the ring of formal power series generated by a free
monoid. This is joint work with Cockett\, Jacqmin and Scott. \n\nWe'll al
so present some results of Beauvais-Fiesthauer\, Dewan and Drummond on the
embedding of topological spaces into finiteness spaces and discuss how th
is might be of use in the analysis of etale groupoids and their C*-algebra
s.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Derivatives of Existentially Regular Trace Languages - Hendrik Maa
rand\, Tallinn University of Technology
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181126T104500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181126T114500
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:722
DESCRIPTION:We provide syntactic (expression-level) language derivative op
erations\, both in the styles of Brzozowski and Antimirov\, for trace clos
ures of regular word languages wrt. an independence relation on the alphab
et. The Brzozowski and Antimirov style derivatives essentially define func
tional resp. relational small-step operational semantics of an (abstracted
) sequential programming language where some instructions\, given by the i
ndependence relation\, can be reordered without any observable consequence
s. Our development is motivated by the fact that some aspects of relaxed m
emories can be explained by allowing the threads of a concurrent program t
o be reordered in this manner.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Random Language Model: a path to principled complexity - Eric Degi
uli\, ENS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181204T112000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181204T122000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:743
DESCRIPTION:Many complex generative systems use languages to create struct
ured objects. We consider a model of random languages\, defined by weighte
d context-free grammars. As the distribution of grammar weights broadens\,
a transition is found from a random phase\, in which sentences are indist
inguishable from noise\, to an organized phase in which nontrivial informa
tion is carried. This marks the emergence of deep structure in the languag
e\, and can be understood by a competition between energy and entropy.
LOCATION:Amphi Turing\, Bâtiment Sophie Germain
END:VEVENT
BEGIN:VEVENT
SUMMARY:Les multiples facettes de la « construction de Grothendieck » -
Jean Bénabou
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190108T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190108T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:745
DESCRIPTION:Je rappelle\, pour fixer les notations\, que si S est une cat
égorie\, et F: S° —> CAT est un lax foncteur\, cette construction four
nit une catégorie Gr(F) munie d’une préfibration Pr(F): Gr(F)—>S qui
est une fibration ssi F est un pseudo-foncteur.\nQuestions:\nPar quel typ
e de bi\, ou 2\, catégorie K peut on remplacer CAT ?\nQuelles propriété
a la correspondance F —> Gr(F)\nPeut-on internaliser cette construction
i.e. si E est\, par exemple\, un topos\, peut-on remplacer S par une cat
égorie interne à E et CAT par la 2-catégorie CAT(E) des catégories int
ernes à E.\nLa liste ci-dessus est loin d’être exhaustive. Je tâchera
i\, sans lasser l’auditoire\, de montrer la grande variété des questio
ns...\, et des réponses.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Types by Need (joint work with Beniamino Accattoli and Maico Leber
le) - Giulio Guerrieri\, Università di Bologna
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190129T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190129T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:747
DESCRIPTION:A cornerstone of the theory of λ-calculus is that intersectio
n types characterise termination properties. They are a flexible tool that
can be adapted to various notions of termination\, and that also induces
adequate denotational models.\nSince the seminal work of de Carvalho in 20
07\, it is known that multi types (i.e. non-idempotent intersection types)
refine intersection types with quantitative information and a strong conn
ection to linear logic. Typically\, type derivations provide bounds for ev
aluation lengths\, and minimal type derivations provide exact bounds.\nDe
Carvalho studied call-by-name evaluation\, and Kesner used his system to s
how the termination equivalence of call-by-need and call-by-name. De Carva
lho’s system\, however\, cannot provide exact bounds on call-by-need eva
luation lengths.\nIn this paper we develop a new multi type system for cal
l-by-need. Our system produces exact bounds and induces a denotational mod
el of call-by-need\, providing the first tight quantitative semantics of c
all-by-need.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Semantics of higher-order probabilistic programs with conditioning
- Fredrik Dahlqvist\, UCL - Department of Computer Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190128T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190128T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:756
DESCRIPTION:We present a denotational semantics for higher-order probabili
stic programs in terms of linear operators between Banach spaces. Our sema
ntics is rooted in the classical theory of Banach spaces and their tensor
products\, but bears similarities with the well-known semantics of higher-
order programs à la Scott through the use ordered Banach spaces which all
ow definitions in terms of fixed points. Being based on a monoidal rather
than cartesian closed structure\, our semantics effectively treats random
ness as a resource.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Behavioural Type-Based Static Verification Framework for Go - Nobu
ko Yoshida\, Imperial College London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190201T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190201T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:769
DESCRIPTION:The talk gives an overview of our several works on programming
language Go\n\nPOPL'17 Fencing off go: liveness and safety for channel-ba
sed programming\nICSE'18 A Static Verification Framework for Message Pass
ing in Go using Behavioural Types\nPOPL'19 Distributed Programming Using R
ole Parametric Session Types in Go.\n\nGo is a production-level statically
typed programming language whose design features explicit message-passing
primitives and lightweight threads\, enabling (and encouraging) programme
rs to develop concurrent systems where components interact through communi
cation more so than by lock-based shared memory concurrency. Go can detect
global deadlocks at runtime\, but does not provide any compile-time prote
ction against all too common communication mismatches and partial deadlock
s.\nWe present a static verification framework for liveness and safety in
Go programs\, able to detect communication errors and deadlocks by model c
hecking. Our toolchain infers from a Go program a faithful representation
of its communication patterns as behavioral types\, where the types are mo
del checked for liveness and safety. We also present a recent code generat
ion for Go.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Expedient Algebra: Duality and Entropy Conservation - Michel Schel
lekens\, University College Cork
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190318T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190318T150000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:798
DESCRIPTION:We introduce a new type of algebra\, the Expedient Algebra EXP
\, for which computations satisfy tight distribution control. Algorithms s
atisfying such distribution control are guaranteed to support modular time
analysis--drastically simplifying static timing. The property ensures tha
t problematic algorithms\, for which the exact time is too hard or impossi
ble to analyze with current means can be distinguished at code level from
algorithms supporting an elegant modular time analysis. Little is known ab
out the intrinsic properties of algorithms exhibiting such distribution co
ntrol.\n\nWe show that EXP-computations\, made reversible through history-
keeping\, act as closed systems in which entropy is conserved. Thus modula
rity of timing is linked to entropy conservation of data flow\, sharpening
traditional entropy preservation guaranteed by the second law of thermody
namics for reversible systems. This type of conservation typically holds f
or the case of energy\, but not for entropy. A salient point is that for a
lgorithms satisfying distribution control\, entropy is neither created nor
destroyed\, merely transferred from one form\, i.e. quantitative entropy\
, to another\, i.e. positional entropy.\n\nWe establish the Entropy Conser
vation Laws ECL-1 and ECL-2. ECL-1 expresses the inverse proportionality o
f positional and quantitative entropy for distributions over series-parall
el orders and their duals. ECL-2\, a computational version of entropy cons
ervation\, expresses that order established by the expedient product (with
history) on labels is proportionally destroyed on indices by a shadow tra
nsformation in the dual space. The laws shed new light on the properties o
f algorithms for which distribution control\, and hence modular timing\, i
s guaranteed.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:L'algèbre universelle supérieur dans la théorie des types depen
dants - Eric Finster\, INRIA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190226T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190226T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:809
DESCRIPTION:La traduction naïve des structures ensemblistes dans la théo
rie des types de Martin-Lof est souvent incomplète: sans hypothèses auxi
liaires\, comme la decidabilité de l'égalité ou troncation\, ces traduc
tions ne spécifient pas le comportement de la structure par rapport aux
égalités supérieures. Par contre\, une description complète n'est pas
facile puisque celle-ci exige un nombre infini d'équations. Je présente
rai des progrès récent sur ce problème en donnant une définition d'une
"monade polynomiale" interne à la théorie\ndes types.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Categorical approaches to bisimilarity - Jérémy Dubut\, NII\, To
kyo
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190402T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190402T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:816
DESCRIPTION:There are different categorical approaches to variations of tr
ansition systems and their bisimulations. One is coalgebras\, another one
is open maps. In this talk\, I will describe these two approaches\, illust
rated by the case of labelled transition systems (almost no knowledge in c
ategory theory is needed for this part). I will then describe how it is po
ssible to translate one into the other in some cases. From open maps to co
algebras\, this was done by Lasota\, using multi-sorted transition systems
. From coalgebras to open maps\, this was done in my joint work with Thors
ten Wißmann\, Shin-ya Katsumata and Ichiro Hasuo\, where we derived path-
categories and trace semantics for free for different flavors of categorie
s of coalgebras with non-deterministic branching. I will illustrate those
constructions on various concrete examples (tree automata\, regular nomina
l automata\, …).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Guarded Recursion for Probabilistic Programming and Probabilistic
Logic - Henning Basold\, Leiden University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190702T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190702T150000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:913
DESCRIPTION:Recursion is a great tool to create readable programs and for
proof\ndiscovery. Unrestricted recursion\, however\, leads to non-terminat
ion\nand thereby makes reasoning about programs harder and may make a logi
c\ninconsistent. Guarded recursion\, on the other hand\, allows us to cont
rol\nrecursion in programs and proofs. The basic idea is to extend types o
r\nformulas with a modality\, usually called the later modality\, and a fe
w\nrules that allow the controlled introduction of recursion. This control
\nensures termination of programs and consistency of proofs.\n\nIn this ta
lk\, I will first show how a fibration can be extended\, under\nmild condi
tions\, to a fibration with guarded recursion. The abstract\nsettings of f
ibrations allows the application of guarded recursion in\nvarious settings
such as probabilistic programming and reasoning. We\nwill see this in the
second part of the talk in action\, where we will\ndevise a language for
coinductive probabilistic processes based on\nguarded recursion that retai
ns termination. The semantics of this\nlanguage is obtained by applying th
e construction from the first part\nof the talk to quasi-Borel spaces. Thi
s gives an alternative language\nwith guaranteed termination to the probab
ilistic language with\nunrestricted recursion recently given by Vákár et
al. (POPL'19).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:History-Dependent Nominal μ-Calculus - Clovis Eberhart\, National
Institute of Informatics\, Tokyo
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191008T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191008T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:956
DESCRIPTION:The μ-calculus with atoms\, or nominal μ-calculus\, is a\nte
mporal logic for reasoning about transition systems that operate on\ndata
atoms coming from an infinite domain and comparable only for\nequality. I
t is\, however\, not expressive enough to define some\nproperties that are
of interest from the perspective of system\nverification. To rectify thi
s\, we extend the calculus with tests for\natom freshness with respect to
the global history of transitions.\nSince global histories can grow arbitr
arily large\, it is not clear\nwhether model checking for the extended cal
culus is decidable. We\nprove that it is\, by showing that one can restri
ct attention only to\nlocally relevant parts of the history.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Topos theoretic approaches to formal model theory - Ivan Di Libert
i\, Masaryk University (Brno)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191203T111500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191203T121500
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:999
DESCRIPTION:Accessible categories with directed colimits have proven to be
a suitable framework to develop abstract model theory and generalize the
notion of abstract elementary class\, quite relevant in model theory. For
every accessible category with directed colimits A\, one can define its Sc
ott topos S(A). This construction is the categorification of the Scott top
ology over a poset with directed unions\, and thus provides a geometric un
derstanding of accessible categories. S(A) represents also a candidate axi
omatization of A\, in the sense that the category of points of the Scott t
opos (i.e.\, the models of the theory that it classifies) is very often a
relevant hull of A. During the talk we introduce the Scott construction an
d explain both its geometric and logical aspects.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A probabilistic approach to floating point arithmetic - Fredrik Da
hlqvist\, University College London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191119T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191119T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1006
DESCRIPTION:Finite-precision floating point arithmetic introduces rounding
errors which are traditionally bounded using a worst-case analysis. Howev
er\, worst-case analysis might be overly conservative because worst-case e
rrors can be extremely rare events in practice. Here we develop a probabil
istic model of rounding errors with which it becomes possible to quantify
the likelihood that the rounding error of an algorithm lies within a given
interval. \n\nGiven an input distribution\, the model requires the distri
bution of rounding errors. We show how to exactly compute this distributio
n for low precision arithmetic. For high precision arithmetic we derive a
simple but surprisingly useful approximation. The model is then entirely c
ompositional: given a numerical program written in a simple imperative pro
graming language we can recursively compute the distribution of rounding e
rrors at each step and propagate it through each program instruction. This
is done by applying a formalism originaly developed by Kozen to understan
d the semantics of probabilistic programs\, for example how probability di
stributions gets transformed by assignments or "if then else" statements.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Quantum Programming with Inductive Datatypes: Causality and Affine
Type Theory - Vladimir Zamdzhiev\, Tulane University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191126T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191126T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1018
DESCRIPTION:Inductive datatypes in programming languages allow users to de
fine useful data structures such as natural numbers\, lists\, trees\, and
others. In this talk we discuss how inductive datatypes may be added to th
e quantum programming language QPL. We construct a sound categorical model
for the language and by doing so we provide the first detailed semantic t
reatment of user-defined inductive datatypes in quantum programming. We al
so show our denotational interpretation is invariant with respect to big-s
tep reduction\, thereby establishing another novel result for quantum prog
ramming. Compared to classical programming\, this property is considerably
more difficult to prove and we demonstrate its usefulness by showing how
it immediately implies computational adequacy at all types. To further cem
ent our results\, our semantics is entirely based on a physically natural
model of von Neumann algebras\, which are mathematical structures used by
physicists to study quantum mechanics. Joint work with Romain Péchoux\, S
imon Perdrix and Mathys Rennela.
LOCATION:Salle 3014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Extensional and Intensional Semantic Universes: A Denotational Mod
el of Dependent Types - Valentin Blot\, INRIA\, ENS Paris-Saclay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191203T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191203T110000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1020
DESCRIPTION:We describe a dependent type theory\, and a denotational model
for it\,\nthat incorporates both intensional and extensional semantic uni
verses.\nIn the former\, terms and types are interpreted as strategies on
certain\ngraph games\, which are concrete data structures of a generalized
form\,\nand in the latter as stable functions on event domains. \nThe con
crete data structures themselves form an event domain\, with\nwhich we may
interpret an (extensional) universe type of (intensional)\ntypes. A depen
dent game corresponds to a stable function into this\ndomain\; we use its
trace to define dependent product and sum\nconstructions as it captures pr
ecisely how unfolding moves combine with\nthe dependency to shape the poss
ible interaction in the game. Since\neach strategy computes a stable funct
ion on CDS states\, we can lift\ntyping judgements from the intensional to
the extensional setting\,\ngiving an expressive type theory with recursiv
ely defined type families\nand type operators.\nWe define an operational s
emantics for intensional terms\, giving a\nfunctional programming language
based on our type theory\, and prove\nthat our semantics for it is comput
ationally adequate. By extending it\nwith a simple non-local control opera
tor on intensional terms\, we can\nprecisely characterize behaviour in the
intensional model.\nWe demonstrate this by proving full abstraction and f
ull completeness\nresults.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:From representing recursive and impure programs in Coq to a modula
r formal semantics of LLVM IR - Yannick Zakowski\, Irisa/Inria
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191217T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191217T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1024
DESCRIPTION:The DeepSpec research project is a cross institution\, cross p
roject investigation to push further the science of specification and veri
fication of software artifacts. Its ambition is crystallized into four qua
lities that specifications should have: they should be rich\, live\, two-s
ided and formal.\n\nIn this talk\, we will focus on the design and impleme
ntation of Interaction Trees (ITrees)\, a general-purpose data-structure f
or representing in Coq potentially divergent\, effectful\, programs. ITree
s are built out of uninterpreted events and their continuations. They supp
ort compositional construction of interpreters from event handlers\, which
give meaning to events by defining their semantics as monadic actions. Th
ey are expressive enough to represent impure and potentially nonterminatin
g\, mutually recursive computations in Coq. Finally\, they give rise to a
theory enabling equational reasoning\, up to weak bisimulation\, about ITr
ees and monadic computations built from them. In contrast to other approac
hes\, ITrees are executable via code extraction.\n\nITrees are expressive
enough to serve as a language of specification for most projects of the De
epSpec ecosystem\, making them a sort of Franca Lingua for formal specific
ation\, and helping in connecting projects together. Furthermore\, their a
bility to be extracted make them compatible with ambitions of liveness and
two-sidedness.\n \nIn a second part of this talk\, we will focus on how
ITrees are used in one of the DeepSpec projects in particular: Vellvm. Mo
re specifically\, we will give an account of the ongoing effort to use ITr
ees as a mean to define a modular formal semantics of LLVM IR.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Weak adjoint functor theorems and accessible infinity-cosmoi - Joh
n Bourke\, Masaryk University (Brno)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200122T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200122T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1035
DESCRIPTION:The General Adjoint Functor Theorem of Freyd has a straightfor
ward extension to the enriched setting. There is also a Weak Adjoint Funct
or Theorem\, due to Kainen\, and providing a sufficient condition for the
existence of a weak left adjoint\, where weakness refers to the existence
but not uniqueness of factorizations. I will report on recent joint work w
ith Steve Lack and Lukas Vokrinek\, in which we prove a weak adjoint funct
or theorem in the enriched context. This actually contains the other three
theorems as special cases. Our base for enrichment will be a monoidal mod
el category. Our motivating example involves simplicially enriched categor
ies\, where the base category of simplicial sets is equipped with the Joya
l model structure. The theorem then has applications to the Riehl-Verity t
heory of infinity-cosmoi.
LOCATION:Salle 3014
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Turing-complete extension of first-order logic - Antti Kuusisto\
, University of Helsinki
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200128T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200128T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1036
DESCRIPTION:We discuss a simple Turing-complete extension of first-order l
ogic FO. The extension adds two new features to FO. The first one of these
is the capacity to add new points to models and new tuples to relations\;
the corresponding deletion operators are also introduced. The second new
feature is a construct that allows formulae to refer to themselves. We sur
vey some of the principal properties of this logic and its extensions with
\, e.g.\, generalized quantifiers.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Une approche graphique des systèmes concurrents - Robin Piedeleu\
, University College London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200107T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200107T120000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1045
DESCRIPTION:Cet exposé sera une introduction à l'algèbre linéaire grap
hique (graphical linear algebra)\, un langage qui permet de raisonner de f
açon compositionnelle à propos de système R-linéaires\, pour divers se
mi-anneaux R. Lorsque que R est un corps\, sa sémantique et sa théorie
équationnelle sont bien comprises. Dans ce contexte\, l'algèbre linéair
e graphique est proche des signal flow graphs\, un autre langage communém
ent utilisé en théorie du contrôle pour spécifier des systèmes dynami
ques au comportement linéaire. Des travaux récents ont montrés que\, po
ur R = ℕ\, la même syntaxe graphique permet de spécifier des systèmes
concurrents qui manipulent des ressources discrètes. On obtient alors un
langage suffisamment expressif pour y encoder très naturellement tous le
s réseaux de Petri et raisonner de façon modulaire à propos de leur com
portement. Nous donnerons des axiomatisations complètes pour ces différe
ntes interprétations et étudierons leurs extensions affines. \n\nIl s'ag
it de travaux en collaboration avec Filippo Bonchi\, Pawel Sobocinski et F
abio Zanasi.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The symmetries of spheres in univalent foundations - Pierre Cagne\
, Université de Bergen (Norvège)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200303T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200303T113000
DTSTAMP;VALUE=DATE-TIME:20201126T160301Z
UID:1102
DESCRIPTION:The goal of this work is to get a better understanding of the
type Sn=Sn where Sn is the sphere of dimension n\, inductively defined by
repeated suspensions.\nI will first prove in full details that S1=S1 is eq
uivalent to S1+S1 (the disjoint sum of two copies of the circle)\, and exp
lain why it is highly unrealistic to conjecture a straightforward generali
zation for Sn. However\, part of the argument for S1 can be extended in hi
gher dimensions to prove that Sn=Sn has two equivalent connected component
s\, one centered at the identity function and one centered at its "opposit
e" (to be defined properly during the talk).\nThis generalization is done
by induction on n\, and the case n=1 does not constitutes a good base case
. Consequently I will detail the case n=2 (interesting in its own)\, and s
ketch the induction step for n>3. This is joint work with M.Bezem and N.Kr
aus.
LOCATION:Salle 4033
END:VEVENT
END:VCALENDAR