BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Google Inc//Google Calendar 70.9054//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
DESCRIPTION:Preuves\, programmes et systèmes seminar of IRIF
NAME:Preuves\, programmes et systèmes
REFRESH-INTERVAL:PT4H
TIMEZONE-ID:Europe/Paris
X-WR-CALDESC:Preuves\, programmes et systèmes seminar of IRIF
X-WR-CALNAME:Preuves\, programmes et systèmes
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:String diagrams and the algebra of entanglement - Amar Hadzihasano
vic\, Oxford University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160114T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160114T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:5
DESCRIPTION:The GHZ and W states are two entangled quantum states of three
qubits\, that are inequivalent in the sense that one cannot be turned int
o the other by local (single-qubit) operations\; this is reflected in thei
r different communicational properties and use in cryptographic protocols.
A few years ago\, Coecke and Kissinger showed that one can associate\, to
the two states\, two Frobenius algebras in the category of Hilbert spaces
- a type of algebra with a well-understood string diagram representation\
, which could hopefully provide a bridge between algebraic\, computational
and topological aspects of quantum entanglement. We present a complete gr
aphical axiomatisation of the relations between the GHZ and W states/algeb
ras: the ZW calculus. This calculus refines the pre-existing ZX calculus\,
while keeping its most desirable characteristics\, such as the undirected
ness of diagrams\; comes with an explicit normalisation procedure\; provid
es an original decomposition of the category of qubits\, with a prominent
"fermionic" fragment\; and hints at a topological explanation of its compo
nents and axioms.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Complexity Constraints as Group Actions - Thomas Seiller\, Departm
ent of Computer Science\, University of Copenhagen - DIKU
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160310T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160310T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:11
DESCRIPTION:The purpose of this talk is to explain a new approach to compl
exity theory based on (dynamic) semantics of linear logic\, whose aim is t
o enable techniques and invariants from ergodic theory (e.g. l^2-Betti num
bers of a countable Borel equivalence relation) to be used in computationa
l complexity.\n\nThe origins of the techniques can be traced to Girard's
“geometry of interaction” (GoI) program using von Neumann algebras and
the recent GoI-inspired results in complexity. However\, this approach re
aches its full strength when using the more combinatorial setting of Inter
action Graphs models of (fragments of) linear logic. Using techniques akin
to game semantics (with a bit of measure theory)\, we are able to charact
erise (predicate) complexity classes as the set of programs/proofs interpr
etations of type Pred[m] := Nat => Bool. These models are parametrised by
a group of measure-preserving maps m (equivalently\, by a measurable group
action) and provide the first sketches of a conjectured correspondence be
tween measurable group actions and complexity constraints.
LOCATION:Salle du Conseil
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA - Pawel Sobocinski\, University of Southampton
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160324T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160324T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:12
DESCRIPTION:
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Enriched-adjunction models and polarisation for modelling effects
and resources - Guillaume Munch-Maccagnoni\, Cambridge Computer lab
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160330T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160330T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:13
DESCRIPTION:(joint work with Marcelo Fiore and Pierre-Louis Curien)\n\nI w
ill present “linear call-by-push-value” enriched-adjunction models ref
ining call-by-push-value models of effects and linear/non-linear models of
linear logic\, with higher-order functions\, sums\, and resource modaliti
es\, together with a theorem lifting linear models into cartesian ones. I
will also present computational interpretations of these models as intuiti
onistic (linear) logics (LJ/ILL) where the order of evaluation matters\, i
n the form of polarised calculi that satisfy usual properties of Barendreg
t-style lambda-calculus\, and that have sound and coherent interpretations
in the previous models. This suggests an approach to modelling proofs and
programs with direct models and calculi.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Preciseness of Subtyping on Intersection and Union Types - Silvia
Ghilezan\, Université de Novi Sad
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160421T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160421T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:54
DESCRIPTION:The notion of subtyping has gained an important role both in t
heoretical and applicative domains: in lambda and concurrent calculi as we
ll as in programming languages. The soundness and the completeness\, toget
her referred to as the preciseness of subtyping\, can be considered from t
wo different points of view: denotational and operational. The former prec
iseness is based on the denotation of a type which is a mathematical objec
t that describes the meaning of the type in accordance with the denotation
s of other expressions from the language. The latter preciseness has been
recently developed with respect to type safety\, i.e. the safe replacement
of a term of a smaller type when a term of a bigger type is expected.\n\n
We propose a technique for formalising and proving operational preciseness
of the subtyping relation in the setting of a concurrent lambda calculus
with intersection and union types. The key feature is the link between typ
ings and the operational semantics. We prove then sound- ness and complete
ness getting that the subtyping relation of this calculus enjoys both deno
tational and operational preciseness. \n\nThis is a joint work with Marian
giola Dezani-Ciancaglini.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Infinitary Lambda Calculi from a Linear Perspective - Ugo Dal Lago
\, Univ. Bologna
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160602T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160602T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:76
DESCRIPTION:We introduce a linear infinitary lambda-calculus in which two
exponential modalities are available\, the first one being the usual\, fin
itary one\, the other being the only construct interpreted coinductively.
The obtained calculus embeds the infinitary applicative lambda-calculus an
d is universal for computations over infinite strings. What is particularl
y interesting about the calculus is that the refinement induced by linear
logic allows to restrict both modalities so as to get calculi which are te
rminating inductively and productive coinductively. We exemplify this idea
by isolating a fragment of the calculus around the principles of SLL and
4LL. Interestingly\, it enjoys confluence\, contrarily to what happens in
ordinary infinitary lambda-calculi.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Bayesian inversion by ω-complete cone duality - Vincent Danos\, E
NS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160929T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160929T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:118
DESCRIPTION:The process of inverting Markov kernels relates to the importa
nt subject of Bayesian modelling and learning. In fact\, Bayesian update i
s exactly kernel inversion. We investigate how and when Markov kernels
(aka stochastic relations\, or probabilistic mappings) can be inverted. We
address the question both directly on the category of measurable spaces\,
and indirectly by interpreting kernels as Markov operators:\nFor the dire
ct option\, we introduce a typed version of the category of Markov kernels
and use the so-called ‘disintegration of measures’. Here\, one has to
specialise to measurable spaces borne from a simple class of topological
spaces -e.g. Polish spaces (other choices are possible). Our method and re
sult greatly simplify a recent development by Culbertson and Sturz.\nFo
r the operator option\, we use a cone version of the category of Markov op
erators (aka kernels seen as predicate transformers). That is to say
\, our linear operators are not just continuous\, but are required to sati
sfy the stronger condition of being ω-chain-continuous. Prior work
shows that one obtains an adjunction in the form of a pair of contravarian
t and inverse functors between the categories of L1- and L∞-cones. Inver
sion\, seen through the operator prism\, is just adjunction. No topo
logical assumption is needed.\nWe show that both c
ategories (Markov kernels and ω-chain-continuous
Markov operators) are related by a family of contravariant functors Tp for
1 ≤ p ≤ ∞. The Tp’s are Kleisli extensions of (duals of) conditio
nal expectation functors introduced before.\nWe prove that
both notions of inversion agree when both defined: if
f is a kernel\, and f† its direct inverse\, then T∞(f)† = T1(f†).
\nThis is a joint work with Fredrik Dahlqvist UCL\, Ohad Kammar Oxford\,
Ilias Garnier ENS
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:New Results on Morris's Observational Theory --- The Benefits of S
eparating the Inseparable - Giulio Manzonetto\, LIPN
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161006T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161006T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:119
DESCRIPTION:We study the theory of contextual equivalence in the untyped\n
lambda-calculus\, generated by taking the normal forms as observables.\nIn
troduced by Morris in 1968\, this is the original extensional lambda\ntheo
ry H+ of observational equivalence. On the syntactic side\, we show\nthat
this lambda-theory validates the omega-rule\, thus settling a\nlong-standi
ng open problem. On the semantic side\, we provide\nsufficient and necessa
ry conditions for relational graph models to be\nfully abstract for H+. We
show that a relational graph model captures\nMorris's observational pre-o
rder exactly when it is extensional and\nlambda-König. Intuitively\, a mo
del is lambda-König when every\nlambda-definable tree has an infinite pat
h which is witnessed by some\nelement of the model.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Optimisation de programmes C++ concurrents - Thibaut Balabonski\,
LRI\, Université Paris Sud
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161124T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161124T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:131
DESCRIPTION:
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Exposé repoussé à début 2017 - Bruno Barras
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161117T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161117T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:132
DESCRIPTION:
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Operational Nominal Game Semantics - Guilhem Jaber\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161103T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161103T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:137
DESCRIPTION:We introduce a fully-abstract intensional model for a polymorp
hic call-by-value language with higher-order references.\nAs in game seman
tics\, the denotation of a term is represented as a set of plays between t
he term and its environment. But rather than building it compositionally\,
by induction over the term\, we generate it using a labelled transition s
ystem representing all the possible interactions between the term and any
environment.\nNames\, and more generally the theory of nominal sets\, are
crucially used to represent locations (i.e. memory addresses) and function
al and polymorphic values. Freshness of such names then control the observ
ational power of environments.\nThanks to the presence of references\, the
observational power of environments is strong enough to avoid the need of
performing a quotient of the model to be fully abstract. This gives us ne
w principles to reason on effectul and polymorphic programs.\nThis work ha
s been done in collaboration with Nikos Tzevelekos (QMUL).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Building Graphical Choreographies From Communicating Machines: Pri
nciples and Applications - Julien Lange\, Imperial College
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161201T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161201T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:152
DESCRIPTION:Graphical choreographies\, or global graphs\, are general mult
iparty\nsession specifications featuring expressive constructs such as for
king\,\nmerging\, and joining for representing application-level protocols
.\nGlobal graphs can be directly translated into modelling notations such\
nas BPMN and UML.\nIn the first part of the talk\, I will first present an
algorithm whereby\na global graph can be constructed from asynchronous in
teractions\nrepresented by communicating finite-state machines (CFSMs)\; a
nd a sound\ncharacterisation of a subset of safe CFSMs from which global g
raphs can\nbe constructed.\nIn the second part\, I will outline a few rece
nt applications of this\nwork to communicating timed automata and the Go p
rogramming language.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dynamic programming and coalgebras with sharing - Tarmo Uustalu\,
Tallinn University of Technology
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170126T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170126T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:187
DESCRIPTION:Dynamic programming is about exploiting sharing opportunities
in\nrecursive call trees of a function. If the pattern of sharing\nopportu
nities is known statically\, a call dag can be built instead of\na tree fr
om the start.\n\nIn this talk\, we present a generic framework for doing s
o and\ndemonstrate it in action on two textbook examples of dynamic\nprogr
amming - Fibonacci and edit distance. We describe sharing\nopportunity pat
terns with systems of equations between node\naddresses. A technique from
term rewriting systems\, namely\nKnuth-Bendix completion\, gives us unique
normal forms for node\naddresses. A dag is represented as a spanning tree
whose nodes are\ndefined by addresses in normal form. Mathematically\, th
e function\ntaking an input for our function of interest into a call tree
is a\ncomonad coalgebra\, node addresses are coterms and equations are\nco
equations.\n\nA Haskell implementation of this framework uses circular pro
gramming\nand a generic implementation of derivatives of functors.\n\nWe v
iew this work as a showcase of how basic algorithmics and more\nadvanced c
ategory theory can interact in a mutually beneficial way.\n\nThis joint wo
rk with Nicolas Wu\, University of Bristol.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sur des modèles algébriques d'infini-n-catégories faibles cubiq
ues - Camell Kachour\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170110T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170110T120000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:188
DESCRIPTION:
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:An Algebraic Combinatorial Approach to the Abstract Syntax of Opet
opic Structures - Marcelo Fiore\, University of Cambridge
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170223T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170223T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:204
DESCRIPTION:The starting point of the talk will be the identification of s
tructure common\nto tree-like combinatorial objects\, exemplifying the sit
uation with abstract\nsyntax trees~(as used in formal languages) and with
opetopes (as used in\nhigher-dimensional algebra). The emerging mathemati
cal structure will be then\nformalized in a categorical setting\, unifying
the algebraic aspects of the\ntheory of abstract syntax of [2\,3] and the
theory of opetopes of [5]. This\nrealization conceptually allows one to
transport viewpoints between these\, now\nbridged\, mathematical theories
and I will explore it here in the direction of\nhigher-dimensional algebra
\, giving an algebraic combinatorial framework for a\ngeneralisation of th
e slice construction of [1] for generating opetopes. The\ntechnical work
will involve setting up a microcosm principle for\nnear-semirings and subs
equently exploiting it in the cartesian closed\nbicategory of generalised
species of structures of [4]. Connections to\n(cartesian and symmetric mo
noidal) equational theories\, lambda calculus\, and\nalgebraic combinatori
cs will be mentioned in passing.\n\n[1] J.Baez and J.Dolan. Higher-Dimens
ional Algebra III. n-Categories and the\nAlgebra of Opetopes. Advances i
n Mathematics 135\, pages 145-206\, 1998.\n\n[2] M.Fiore\, G.Plotkin and D
.Turi. Abstract syntax and variable binding. \nIn 14th Logic in Computer
Science Conf. (LICS'99)\, pages 193-202. IEEE\,\nComputer Society Press\
, 1999.\n\n[3] M.Fiore. Second-order and dependently-sorted abstract synt
ax. In Logic\nin Computer Science Conf. (LICS'08)\, pages 57--68. IEEE\,
Computer Society\nPress\, 2008. \n\n[4] M.Fiore\, N.Gambino\, M.Hyland\,
and G.Winskel. The cartesian closed\nbicategory of generalised species of
structures. In J. London Math. Soc.}\, \n77:203-220\, 2008. \n\n[5] S.Sz
awiel and M.Zawadowski. The web monoid and opetopic sets. In\narXiv:1011
.2374 [math.CT]\, 2010.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Verifying properties of functional programs: from the deterministi
c to the probabilistic case - Charles Grellois\, INRIA - Univ. Bologna (It
alie)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170316T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170316T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:215
DESCRIPTION:In functional programs\, also called higher-order programs\, f
unctions may take functions themselves as arguments. As a result\, their m
odel-checking relies in most approaches on semantic or type-theoretic tool
s. In this talk\, I will explain how an analysis based on linear logic of
a model-checking result of 2009 by Kobayashi and Ong led Melliès and I to
the construction of a model for model-checking. This model is such that\,
when interpreting a term with recursion representing the tree of traces o
f a functional program\, its denotation determines whether it satisfies a
MSO property of interest. A related and similar model was obtained indepen
dently by Salvati and Walukiewicz.\nIn the second part of the talk\, I wil
l discuss the verification of termination for functional programs with rec
ursion and probabilistic choice. Dal Lago and I defined recently a type sy
stem which is such that typable programs terminate with probability 1. In
other terms\, their set of diverging executions is negligible. If time all
ows\, I will sketch ideas towards an extension of the model-checking resul
ts of the deterministic case to quantitative logics and functional program
s with recursion.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Full Abstraction of the Probabilistic Böhm Trees - Thomas Leventi
s\, Institut de Mathématiques de Marseille
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170323T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170323T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:216
DESCRIPTION:A very natural notion of equivalence of programs is the observ
ational equivalence: two programs are equivalent if they have the same beh
aviour in any environment. More specifically in the lambda-calculus two te
rms M and N are equivalent if for every context C\, the terms C[M] and C[N
] are either both solvable or both unsolvable. Respecting this equivalence
is an important property of some models of the lambda-calculus\, called t
he full abstraction. It is well known that the model of infinitely extensi
onal Böhm trees is fully abstract. The question we are interested in is w
hat becomes of these notions when we introduce probabilistic choice in the
calculus.\n\nThe solvability has a natural extension\, which is the conve
rgence probability\, hence two terms are observationally equivalent if the
y have the same convergence probability under any context. There is also a
simple way to define probabilistic Bohm trees\, as we can associate to an
y term a subprobability distribution over head normal forms. But it is not
obvious that these generalizations of the deterministic notions are still
equivalent. In this talk we will show how to prove that probabilistic Bö
hm trees actually form a model\, and how to get a separability result to e
nsure this model is fully abstract.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Un\, personne et cent mille: a meta theory for testing equivalence
s? - Giovanni Bernardi\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170330T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170330T110000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:217
DESCRIPTION:Testing theory focuses on contextual equivalences\nthat were p
roposed in the 80s as an alternative\nto bisimulation equivalence.\nDuring
the last decade testing equivalences proved\nuseful in constructing seman
tic models\nof session types and in laying the foundations of\nweb-service
technologies. As result\, testing theory\nis more useful and richer than
ever.\nIn this seminar I will recall the chief ideas behind\ntesting theor
y\, and argue that we lack\na general methodology to reason on testing equ
ivalences.\nI will also outline the evidence that a meta-theory\nmay exist
\, and some open questions.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Des arbres sans ambiguités - Bérénice Delcroix-Oger\, Institut
de Mathématiques de Toulouse
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170427T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170427T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:218
DESCRIPTION:Les tableaux boisés sont des objets combinatoires intervenant
notamment dans l'étude de certains modèles de mécanique statistique.\n
Cet exposé porte sur les arbres non ambigus\, qui sont un cas particulier
de tableaux boisés reliés aux permutations ayant leurs excédences (w(i
)>i) en début de mot. Nous avons obtenu\, lors d'un travail commun avec J
.-C. Aval\, A. Boussicault\, F. Hivert et P. Laborde-Zubieta\, des résult
ats énumératifs et bijectifs sur ces objets\, que je présenterai ici ap
rès avoir introduit le cadre de cette étude.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formalizing Compositional Proofs - Jamie Vicary\, Univ. of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170420T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170420T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:219
DESCRIPTION:I will present a new proof assistant\, Globular\, which allows
the\nformalization of compositional proofs in higher category theory. The
\ninterface is geometrical\, with proofs depicted as string diagrams\, and
\nallowing direct click-and-drag manipulation of proofs in a simple and\ni
ntuitive way\, up to the level of 4-categories. I will show how to\nbuild
a simple proof from scratch\, and present some sophisticated\nformalized p
roofs from topology and algebra. I will also give some\ndetails of the the
oretical basis\, which gives a new and simple way to\nunderstand higher ca
tegory theory. This talk will be accessible\, and\nwill not require any pr
evious knowledge.\n\nWeb site: https://ncatlab.org/nlab/show/Globular\nPap
er: https://arxiv.org/abs/1610.06908
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hybrid set-vector automata from a category-theoretic perspective -
Daniela Petrisan\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170330T111500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170330T121500
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:233
DESCRIPTION:The main purpose of this talk is to introduce a new automata\n
model\, hybrid set-vector automata\, that naturally embed deterministic\nf
inite state automata and finite automata weighted over a field.\n\nWe take
a category-theoretic approach\, which provides a neat\nunderstanding of m
inimisation. It is well known that category theory\noffers a unifying view
of some automata theory results. For example\,\nminimisation of determini
stic automata (over finite words) and\nShützenberger’s automata weighte
d over fields\, arise from the same\ncategorical reasons.\n\nIn the first
part of the talk\, I will discuss about how to model and\nminimise automat
a in categories. Traditionally\, automata are seen\neither as algebras for
a functor plus a final map\, possibly in a\nmonoidal category\, or as coa
lgebras for a functor plus an initial\nmap. We propose yet another view of
automata as functors from an input\ncategory to an output category.\n\nTh
e new hybrid set-vector automata can be modelled by taking the\noutput cat
egory to be a free-colimit completion of the category of\nfinite-dimension
al vector spaces under a certain class of colimits.\n\nThis is joint work
with Thomas Colocombet.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The state of the art in gradual typing - Jeremy Siek\, Indiana Uni
versity
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170427T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170427T150000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:242
DESCRIPTION:Gradual typing is an approach for designing programming langua
ges that\nintegrate static and dynamic type checking. Gradual typing gives
the\nprogrammer fine-grained control over which regions of a program are\
nstatically checked and which regions are dynamically checked. Over\nthe
last decade\, there has been renewed interest in such an\nintegration part
ly due to the rise in popularity of dynamic languages.\nBut as small progr
ams grow into large programs\, so does the need for\nearly error detection
and modularity\, which is provided by static type\nchecking. Gradual typ
ing provides a practical migration path for\ndynamically typed programs to
become more statically typed. This talk\nwill give a glimpse at the stat
e of the art in gradual typing. It will\ndescribe a) the major challenges
in the design and implementation of\ngradually typed languages\, b) the re
search that has addressed many of\nof these challenges\, and c) the open p
roblems that need to be solved.\nThe research in gradual typing spans both
theoretical and practical\nquestions\, from mechanized metatheory to effi
cient compilation.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:An interpretation of system F through bar recursion - Valentin Blo
t\, Queen Mary University\, London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170509T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170509T150000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:247
DESCRIPTION:There are two possible computational interpretations of second
-order\narithmetic: Girard's system F or Spector's bar recursion and its\n
variants. While the logic is the same\, the programs obtained from these\n
two interpretations have a fundamentally different computational\nbehavior
and their relationship is not well understood. We make a step\ntowards a
comparison by defining the first translation of system F into\na simply-ty
ped total language with a variant of bar recursion. This\ntranslation reli
es on a realizability interpretation of second-order\narithmetic. Due to G
ödel's incompleteness theorem there is no proof of\ntermination of system
F within second-order arithmetic. However\, for\neach individual term of
system F there is a proof in second-order\narithmetic that it terminates\,
with its realizability interpretation\nproviding a bound on the number of
reduction steps to reach a normal\nform. Using this bound\, we compute th
e normal form through primitive\nrecursion. Moreover\, since the normaliza
tion proof of system F proceeds\nby induction on typing derivations\, the
translation is compositional.\nThe flexibility of our method opens the pos
sibility of getting a more\ndirect translation that will provide an altern
ative approach to the\nstudy of polymorphism\, namely through bar recursio
n.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Découpage d'associativité généralisé - Samuele Giraudo\, Pari
s-Est Marne-la-Vallée
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170615T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170615T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:254
DESCRIPTION:Les algèbres dendriformes sont des structures algébriques in
troduites\npar Loday. Elle offrent un moyen de découper un produit associ
atif en\ndeux produits non nécessairement associatifs. L'étude de ces al
gèbres\,\nréalisée avec le point de vue fourni par la théorie des opé
rades\, fait\napparaître la combinatoire des arbres binaires et des méla
nges d'arbres.\nNous définissons ici une opérade à un paramètre entier
généralisant \nl'opérade diassociative. Par dualité de Koszul\, nous
obtenons des \ngénéralisations de l'opérade dendriforme. Les algèbres
sur ces opérades \npermettent de découper un produit associatif en plusi
eurs parties\, avec \ncertaines relations de compatibilité. Les propriét
és combinatoires et \nalgébriques de ces structures sont passées en rev
ue.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Understanding Computation in Game Semantics - Martin Hyland\, DPMM
S\, University of Cambridge
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171019T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171019T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:316
DESCRIPTION:
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The parallel intensionally fully abstract model for PCF - Simon Ca
stellan\, Imperial College
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171123T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171123T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:356
DESCRIPTION:In this talk\, we introduce a new game semantics framework for
\nconcurrency based on event structures\, extending the work of Rideau and
\nWinskel. In this framework\, we can extend the notions of innocence and\
nwell-bracketing to the concurrent (and non-deterministic) case\,\ngeneral
izing the so-called "Abramsky cube".\n\nThis talk focuses on the determini
stic case. I will first introduce the\nconcurrent strategies and their com
position\, in the existing linear\nsetting. I will then present our extens
ion to nonlinearity using copy\nindices and symmetry to represent uniformi
ty. I will then present our\nnotions of concurrent innocence & well-bracke
ting\, to finish on our\nresult of intensional full abstraction for PCF. T
ime permitting\, I will\ndiscuss extensions of this result to non-angelic
nondeterminism and\nprobabilities.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Linearity in Higher-Order Recursion Schemes - Charles Grellois\, U
niversité Aix-Marseille
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171207T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171207T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:357
DESCRIPTION:In higher-order model-checking (HOMC)\, functional programs ar
e represented as higher-order recursion schemes (HORS)\, a kind of grammar
with parameters which can be functions. These grammars generate infinite
trees\, over which we want to check formulas of monadic second-order logic
(MSO). This problem is decidable\, as proved first by Ong in 2006\, and t
hen by many others including Kobayashi and Ong (2009) whose approach use i
ntersection types. It turns out that linear logic is a powerful and enligh
tening tool to reason about HOMC\, as shown by Grellois and Melliès in th
e last years.\n\nIn general\, the complexity of the HOMC problem is n-EXPT
IME\, where n is the order of the HORS of interest. In this talk\, we expl
ain that we can refine this complexity measure: motivated by linear logic\
, we introduce *linear* HORS and a linear-nonlinear model of automaton che
cking fragments of MSO. We then show that HOMC is in fact n-EXPTIME comple
te for n the *linear* order of the linear HORS generating the tree of inte
rest. We believe that this explains why HOMC\, in spite of its huge theore
tical complexity\, has been successfully used in practice by Kobayashi's t
eam.\n\nThis linear framework allows to reprove in a much simpler way thre
e existing results extending the usual HOMC problem\, and notably to deal
with call-by-value programs in a smooth way (the usual HOMC approach consi
dering call-by-name).\n\nThis is joint work with Pierre Clairambault and A
ndrzej Murawski.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:ENS Lyon - Séminaire Chocola
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171214T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171214T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:362
DESCRIPTION:
LOCATION:ENS Lyon
END:VEVENT
BEGIN:VEVENT
SUMMARY:ENS LYon - Séminaire Chocola
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171109T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171109T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:363
DESCRIPTION:
LOCATION:ENS Lyon
END:VEVENT
BEGIN:VEVENT
SUMMARY:Homenet\, l'IETF\, et le processus de normalisation - Juliusz Chro
boczek\, IRIF\, Université Paris Diderot
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171214T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171214T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:413
DESCRIPTION:Depuis plusieurs années\, je participe au groupe de travail H
omenet de\nl'IETF\, l'organisme qui définit les normes qui régissent l'I
nternet. Dans\ncet exposé\, sur l'exemple de Homenet et de mes aventures
à l'IETF\,\nj'essaierai de donner une idée de ce qu'est le processus de
normalisation\,\npourquoi il est important pour l'Informatique et pour l'
Internet.\n\nCet exposé est une version étendue et légèrement censuré
e de l'exposé que\nj'ai donné aux Journées PPS le 12 octobre 2017.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:From Couplings to Probabilistic Relational Program Logics - Justin
Hsu\, University College of London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180125T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180125T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:439
DESCRIPTION:Many program properties are relational\, comparing the behavio
r of a program (or even two different programs) on two different inputs. W
hile researchers have developed various techniques for verifying such prop
erties for standard\, deterministic programs\, relational properties for p
robabilistic programs have been more challenging. In this talk\, I will su
rvey recent developments targeting a range of probabilistic relational pro
perties\, with motivations from privacy\, cryptography\, machine learning.
The key idea is to meld relational program logics with an idea from proba
bility theory\, called a probabilistic coupling. The logics allow a highly
compositional and surprisingly general style of analysis\, supporting cle
an proofs for a broad array of probabilistic relational properties.\n\nBio
: Justin Hsu is a post-doctoral researcher at the University College of Lo
ndon. He obtained his graduate degree from the University of Pennsylvania.
His research interests span formal verification and theoretical computer
science\, including verification of randomized algorithms\, differential p
rivacy\, and game theory.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Provably secure compilation of side-channel countermeasures: the c
ase of cryptographic "constant-time" - Vincent Laporte\, IMDEA Software
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180208T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180208T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:513
DESCRIPTION:Software-based countermeasures provide effective mitigation ag
ainst\nside-channel attacks\, often with minimal efficiency and deployment
\noverheads. Their effectiveness is often amenable to rigorous analysis:\n
specifically\, several popular countermeasures can be formalized as\ninfor
mation flow policies\, and correct implementation of the\ncountermeasures
can be verified with state-of-the-art analysis and\nverification technique
s. However\, in absence of further justification\,\nthe guarantees only ho
ld for the language (source\, target\, or\nintermediate representation) on
which the analysis is performed.\n\nWe consider the problem of preserving
side-channel countermeasures by\ncompilation for cryptographic “constan
t-time”\, a popular countermeasure\nagainst cache-based timing attacks.
We present a general method\, based\non the notion of 2-simulation\, for p
roving that a compilation pass\npreserves the constant-time countermeasure
. Using the Coq proof\nassistant\, we verify the correctness of our method
and of several\nrepresentative instantiations.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Topology\, Order and Causal Structure - Prakash Panangaden\, McGil
l University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180215T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180215T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:522
DESCRIPTION:The causal structure of spacetime defines a (pair of) natural
order\nstructures on the underlying set of events. Much of the analysis o
f cauasl\nstructure involves a delicate interplay between order\, topology
and\ngeometry. In view of the fundamental role of the causal order in ce
rtain\napproaches to quantum gravity as well as its fundamental role in\nc
oncurrency theory one can ask whether the topology can be derived from\npu
re order theoretic considerations.\n\nIn a remarkable example of serendipi
ty\, order theory has been developed by\ncomputer scientists and mathemati
cians in order to capture computability\nconcepts. Dana Scott developed a
notion of a continuous lattice or\ncontinuous poset with a view to captur
ing computability as continuity with\na suitable topology that has come to
be known as the Scott topology. This\nsubject has acquired the name of `
`domain theory.''\n\nWe applied domain theory to the problem of reconstruc
ting the spacetime\ntopology from the order and came up with a number of r
esults about\nreconstruction of spacetime structure from just a countable
dense set. \n\nWe prove that a globally hyperbolic spacetime with its cau
sality relation\nis a bicontinuous poset whose interval topology is the ma
nifold topology.\nFrom this one can show that from only a countable dense
set of events and\nthe causality relation\, it is possible to reconstruct
a globally hyperbolic\nspacetime in a purely order theoretic manner. The
ultimate reason for this\nis that globally hyperbolic spacetimes belong to
a category that is\nequivalent to a special category of domains called in
terval domains.\n\nThis was joint work with Keye Martin of Naval Research
Laboratories.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rencontres Chocola de Février: Prakash Panangaden\, Justin Hsu &
Thomas Ehrhard - Séminaire Chocola\, ENS Lyon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180208T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180208T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:523
DESCRIPTION:http://chocola.ens-lyon.fr/events/meeting-2018-02-08 \n\n10:30
– 12:00\n Prakash Panangaden (Mc Gill University\, Canada)\n Quan
titative Equational Logic \n\n14:00 – 15:00\n Justin Hsu (University
College London\, UK)\n From Couplings to Probabilistic Relational Progr
am Logics \n\n15:30 – 16:30\n Thomas Ehrhard (IRIF\, Univ. Paris Dide
rot)\n Stable and measurable functions on positive cones: a model of pr
obabilistic functional languages with continuous types
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Failure is Not an Option\, or The Curry-Howard-Shadok corresponden
ce - Pierre-Marie Pédrot\, Max Planck Institute for Software Systems\, Sa
arbrücken\, Germany
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180222T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180222T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:527
DESCRIPTION:No one is without knowing the famous Shadok principle « the m
ore it\nfails\, the more likely it will eventually succeed. » Taking insp
iration\nfrom this unfathomable wisdom\, we came up with a dependent type
theory\nwhich allows failure\, so that we could succeed more in proving th
ings.\nSuch a Shadok theory is justified by translating it away into vanil
la\ndependent theory\, just as a mundane compiler would\, where failing ca
n be\ninterpreted as a call-by-name exception mechanism. En passant\, this
\ngives the first full syntactical model of the Calculus of Inductive\nCon
structions introducing effects.\n\nAlas! The right to fail succeeds a tad
too much\, insofar as the\nresulting Shadock type theory is logically inco
nsistent. Not being\nimpressed in any way\, we put order into this madness
by requiring that\nno exception should ever reach toplevel\, thanks to a
clever use of a\nvariant of Bernardy-Lasson syntactic parametricity. While
the former\nmodel can be thought of as Friedman A-translation applied to
CIC\, the\nlatter is no more than a principled variant of Kreisel's modifi
ed\nrealizability that scales to dependent types. In particular\, it readi
ly\ngives a model of CIC that still has canonicity\, strong normalization
and\ndecidable type-checking\, while featuring new principles typical of\n
modified realizability such as the independence of premises and\nunprovabi
lity of Markov's principle.\n\nhttps://www.pédrot.fr/articles/exceptional
.pdf
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Realizability: denotational semantics for correctness - Valentin B
lot\, LRI
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180329T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180329T150000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:564
DESCRIPTION:There exists a large spectrum of techniques for proving correc
tness of\ncomputer programs. At one end is the Curry-Howard isomorphism\,
in which\na typing procedure automatically checks the correctness of a pro
gram\,\nand at the other end are techniques à la Hoare\, in which non-tri
vial\nreasonning is performed in a logic adapted to the programming langua
ge.\nRealizability can be seen as a mixture of these two approaches: provi
ng\nthat a program realizes a specification is done via a combination of\n
automatic techniques in a Curry-Howard fashion\, and manual proofs of\ncor
rectness of subprograms with respect to some axioms. In my talk I\nwill pr
esent some realizability models where the realizability relation\nis defin
ed semantically: a program realizes a specification if its\ndenotation sat
isfies a property in the model. The denotational models\ninvolved include
game semantics\, continuation models and Scott domains.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Model-checking contextual equivalence of higher-order programs wit
h references. - Guilhem Jaber\, LIP
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180329T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180329T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:565
DESCRIPTION:This talk will present SyTeCi\, the first general automated to
ol to check contextual equivalence for programs written in a typed higher-
order language with references (i.e. local mutable states)\, corresponding
to a fragment of OCaml.\n\nAfter introducing the notion of contextual equ
ivalence\, we will see on some examples why it is hard to prove such equiv
alences (reentrant calls\, private states). As we will see\, such examples
can be found in many different programming languages.\n\nThen\, we will i
ntroduce SyTeCi\, a tool to automatically check such equivalences. This to
ol is based on a reduction of the problem of contextual equivalence of two
programs to the problem of reachability of "error states" in transition s
ystems of memory configurations.\n\nContextual equivalence being undecidab
le (even in a finitary setting)\, so does the non-reachability problem for
such transition systems.\nHowever\, one can apply model-checking techniqu
es (predicate abstraction\, summarization of pushdown systems) to check no
n-reachability via some approximations.\nThis allows us to prove automatic
ally many non-trivial examples of the literature\, that could only be prov
ed by hand before. We will end this talk by the presentation of a prototyp
e implementing this work.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Balade entre logiques linéaires classiques et intuitionnistes - O
livier Laurent\, ENS Lyon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180531T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180531T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:607
DESCRIPTION:On discutera différentes manières de relier syntaxiquement l
a\nlogique linéaire classique (LL) et sa version\nintuitionniste (ILL) :
d'une part à travers la question de la\nconservativité de LL sur ILL (co
ntre-exemples et conditions\nsuffisantes)\, et d'autre part via l'étude d
e non-non traductions\nde LL dans ILL. On montrera que ces traductions per
mettent de\nreprésenter des extensions de LL dans ILL\, mais aussi qu'ell
es\npeuvent être utilisées comme outil pour prouver des propriétés de\
nLL : élimination des coupures et focalisation par exemple.\nCes différe
nts résultats ont été formalisés en Coq à l'aide de la\nbibliothèque
Yalla\, que nous présenterons brièvement.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Intersection Types in Deduction Modulo Theory - Olivier Hermant\,
CRI\, Mines ParisTech
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180628T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180628T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:619
DESCRIPTION:In a 2012 paper\, Richard Statman exhibited an inference syste
m\, based on\nsecond order monadic logic and non-terminating rewrite rules
\, that\nexactly types all strongly normalizable lambda-terms. We show tha
t this\nsystem can be simplified to first-order minimal logic with rewrite
\nrules\, along the Deduction Modulo Theory lines.\n\nWe show that our rew
rite system is terminating and that the conversion\nrule respects weak ver
sions of invertibility of the arrow and of\nquantifiers. This requires add
itional care\, in particular in the\ntreatment of the latter. Then we stud
y proof reduction\, and show that\nevery typable proof term is strongly no
rmalizable and vice-versa.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Higher-Dimensional Automata - Jeremy Dubut\, National Institute of
Informatics Tokyo\, Japan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180705T104500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180705T114500
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:620
DESCRIPTION:I will give a new definition of partial Higher Dimension Autom
ata -- a geometric model for true concurrency -- using lax functors. This
definition is simpler than the original\, and more natural from a categori
cal point of view\, but also matches more clearly the intuition that pHDA
are Higher Dimensional Automata with some missing faces. I will then focus
on trees. Originally\, for example in transition systems\, trees are defi
ned as those systems that have a unique path property. To understand what
kind of unique path property is needed in pHDA\, I will start by looking a
t trees as colimits of paths. From this\, I will deduce that trees are exa
ctly the pHDA with the unique path property modulo a notion of homotopy\,
and without any shortcuts. This property will allow me to prove two intere
sting characterisations of trees: trees are exactly those pHDA that are th
e unfolding of another pHDA\; trees are exactly the cofibrant objects\, mu
ch as in the language of Quillen’s model structures. In particular\, thi
s last characterisation gives the premisses of a new understanding of conc
urrency theory using homotopy theory.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Simplicial sets inside cubical sets - Thomas Streicher\, TU Darmst
adt
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180927T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180927T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:653
DESCRIPTION:(joint work with J. Weinberger)\n\nAbstract: Voevodsky's model
of the Univalence Axion in simplicial\nsets is not constructive as shown
by Coquand et al. To avoid this\nproblem Cohen\, Coquand\, Huber\, Moertbe
rg have constructed in\nCubical Sets a model of a Cubical Type Theory whic
h has\ncomputational meaning.\n\nWe show that simplicial sets form a subto
pos of cubical sets which\nallows one to contructively reason in the latte
r about the former.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Towards A General Guarded Lambda-Calculus - Adrien Guatto\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181004T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181004T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:654
DESCRIPTION:Guarded recursion has emerged as a natural paradigm for progra
mming\nwith infinite data structures in type theory and high-assurance fun
ctional\nlanguages. In the first part of this talk\, I will present some i
ntuitions behind\nguarded recursion\, using programming examples. In a sec
ond part\, I will\ndiscuss ongoing work on a typed lambda-calculus equippe
d with rich facilities\nfor defining and manipulating guarded recursive ty
pes.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Type-Based Analysis for Session Inference - Carlo Spaccasassi\, Mi
crosoft Research Cambridge\, Cambridge (United Kingdom)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181025T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181025T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:673
DESCRIPTION:We propose a type-based analysis to infer the session protocol
s of\nchannels in an ML-like concurrent functional language. Combining and
extending\nwell-known techniques\, we develop a type-checking system that
separates the\nunderlying ML type system from the typing of sessions. Wit
hout using linearity\,\nour system guarantees communication safety and par
tial lock freedom. It also\nsupports provably complete session inference w
ith no programmer annotations. We\nexhibit the usefulness of our system wi
th interesting examples\, including one\nwhich is not typable in substruct
ural type systems.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Journées 2018 - Pôle Preuves\, Programmes Et Systèmes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181108T093000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181108T103000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:680
DESCRIPTION:[[::rencontres:pps2018:]]
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Journées 2018 - Pôle Preuves\, Programmes Et Systèmes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181109T093000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181109T103000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:681
DESCRIPTION:[[::rencontres:pps2018:]]
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Salidou's day - Eric Tanter\, Flavien Breuvart\, Shane Mansfield &
Xavier Leroy\, Chocola meeting in Paris
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181115T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181115T120000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:712
DESCRIPTION:11:00 – 12:30 Éric Tanter (Universidad de Chile & Inria
Paris) - Invited talk: Abstracting Gradual Typing: Principles and Applicat
ion to Gradual Parametricity\n\n Gradual typing enables programming lan
guages to seamlessly combine dynamic and static checking. Language researc
hers and designers have extended a wide variety of type systems to support
gradual typing. These efforts consistently demonstrate that designing a s
atisfactory gradual counterpart to a static type system is challenging\, a
nd this challenge only increases with the sophistication of the type syste
m. Gradual type system designers need more formal tools to help them conce
ptualize\, structure\, and evaluate their designs. Based on an understandi
ng of gradual types as abstractions of static types\, we have developed sy
stematic foundations for gradual typing based on abstract interpretation\,
called Abstracting Gradual Typing (AGT for short). Gradual languages desi
gned with the AGT approach satisfy\, by construction\, the established cri
teria for gradually-typed languages. In this talk\, I will give a brief in
troduction to AGT in a simply-typed setting\, and will then discuss recent
work on a gradual counterpart of System F that enforces relational parame
tricity\, even in the presence of imprecise types.\n\n14:00 – 15:00 F
lavien Breuvart (Université Paris 13) - Invited talk: Graded Types Parame
tricity : Principles and Application to Abstract Interpretation\n\n In
this talk\, we will briefly present the yet-to-start project CoGITARe\, wh
ich aims at developing further graded types expressivity and inference in
order to use them to perform abstract interpretations.\n In a second ti
me\, we give an historic on graded type systems and their expressivity. Th
en\, we will see that this expressivity is limited by a lake of dependency
/parametricity. We will thus explore two ongoing research directions that
adds two very different kind of parametricity to graded types.\n (The p
rovocative title should only be taken as a joke. Despite their apparent si
militudes\, this work and Éric Tanter's have vastly different objectives
and involved different issues and techniques. In particular\, notice that
gradual and graded types are fundamentally different.)\n\n15:30 – 16:30
Shane Mansfield (Univ. of Oxford) - Invited talk: An overview of empiri
cal models\n\n Empirical models are a way of formalising data that aris
es in physical experiments. They were first proposed by Abramsky and Brand
enburger as part of a framework to analyse fundamentally non-classical phe
nomena in quantum systems. Conveniently from a computer science perspectiv
e\, they abstract away from the mathematical baggage of quantum theory and
instead allow the key phenomena to be characterised purely as features of
empirical data. After introducing the basic framework I will discuss some
more recent results and developments\, drawing on joint work with a numbe
r of collaborators. In particular: quantum computations can simply be mode
lled as classical computations with the additional ability to interact wit
h a resource empirical model\; quantitative measures of non-classicality c
an be shown to relate directly to some basic quantum-over-classical comput
ational advantages\; and the beginnings of a category-theoretic approach t
o reasoning about empirical models have emerged.\n\n\n18:00 – 19:00 X
avier Leroy - Lecture: Leçon inaugurale au Collège de France\n\n This
is not part of the CHoCoLa day\, but you might be interested in attending
! See https://www.college-de-france.fr/site/xavier-leroy/inaugural-lecture
-2018-11-15-18h00.htm\n\n The meeting will take place in Bâtiment Soph
ie Germain\, here.\n We will first gather at the 3rd floor of the build
ing\, for a breakfast.\n We will then move for the talk of the morning
(11.00-12.30) to Amphi Turing.\n We will have lunch in room 3052\n I
n the afternoon (14h-16h30)\, we will be in room 1016
LOCATION:Salle 3052 + Amphi Turing + 1016
END:VEVENT
BEGIN:VEVENT
SUMMARY:The intuitionistic calculus that was discovered 6 times - Stéphan
e Graham-Lengrand\, LIX\, CNRS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181122T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181122T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:718
DESCRIPTION:In this talk I will review G4ip\, a simple calculus for\nintui
tionistic propositional logic (IPL) that provides a decision\nprocedure fo
r provability. Its basic mechanisms can be traced back to\nVorob'ev in the
50s\, and were found again by Hudelmaier (88)\, Dyckhoff\n(90)\, Paulson
(91)\, and (with a linear logic flavour)\nLincoln-Scedrov-Shankar (91). In
2015\, Claessen and Rosén presented the\nfastest decision procedure for
IPL\, based on SMT-solving techniques. We\ndescribe their algorithm and sh
ow how it can be seen as a variant of the\naforementioned calculus\, albei
t with key variations that provide\nincreased performance. Their algorithm
relies on a SAT-solver used as a\nblack box and treats intuitionistic ent
ailment as a theory. We show how\nthe recent framework of model-constructi
ng satisfiability for\nSMT-solving could further integrate intuitionistic
reasoning within the\nmain SAT-solving loop. This would constitute an intu
itionistic variant\nof the main algorithm of SAT-solvers\, where Kripke mo
dels are built\ninstead of Boolean models.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Linear Implicative Algebras\, towards a Brouwer-Heyting-Kolmogorov
interpretation of linear logic - Luc Pellissier\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181206T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181206T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:719
DESCRIPTION:Implicative Algebras were recently introduced as a unified fra
mework for\nforcing and realisability\, whose particularity is to interpre
t terms and\nformulæ uniformly.\n\nIn this ongoing work with Alexandre Mi
quel\, we show how linear logic\nfits in this picture: we present a family
of models\, where certain\ncomputational principles are distinguished\, a
nd argue thata it provides\na satisfactory meaning explanation of the conn
ectives of (perfective)\nlinear logic.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:ENS Lyon - Journée Chocola
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181213T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181213T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:720
DESCRIPTION:http://chocola.ens-lyon.fr/events/meeting-2018-12-13/
LOCATION:ENS Lyon
END:VEVENT
BEGIN:VEVENT
SUMMARY:Concurrent strategies for Herbrand's theorem - Aurore Alcolei\, En
s Lyon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190110T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190110T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:738
DESCRIPTION:Herbrand's theorem exposes some of the constructive content of
classical logic. In its simplest form\, it reduces the validity of a firs
t-order purely existential formula to that of a finite disjunction. More g
enerally\, it reduces first-order validity to propositional validity\, by
understanding the structure of the assignment of first-order terms to exis
tential quantifiers\, and the causal dependency between quantifiers.\n\nIn
this talk\, we show that Herbrand's theorem in its general form can be el
egantly stated and proved as a theorem in the framework of concurrent game
s\, a denotational semantics designed to faithfully represent causality an
d independence in concurrent systems. Closely related to expansion trees\,
the causal structure of concurrent strategies\, paired with annotations b
y first-order terms\, is used to specify the dependency between quantifier
s. As furthermore these strategies can be composed we are able to interpre
t classical sequent proofs\, yielding a compositional proof of Herbrand's
theorem.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Linearisation of the lambda-calculus and its termination - Sandra
Alves
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190207T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190207T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:740
DESCRIPTION:The notion of linearisation of the lambda-calculus has been ex
plored in different settings: Damas and Florido used information given by
intersection types\, to define a notion of expansion of terms in the lambd
a-calculus into linear terms\; Kfoury embedded the lambda-calculus into a
new linear calculus\, with a new notion of "linear" reduction\, and linear
ization was defined indirectly by means of a notion of contraction of expa
nded terms in the new calculus into standard lambda-terms\; Alves and Flor
ido defined a notion of linearisation from standard lambda-terms into a li
near subset\, called the weak linear lambda-calculus\, by using the notion
of computation as paths\, deriving from Lévy’s labelled lambda-calculu
s. \n\nIn this talk we will explore these previous works\, discuss their r
elation and present some open problems regarding the termination of linear
isation methods.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA - Seminaire Chocola\, Ens Lyon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190124T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190124T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:741
DESCRIPTION:
LOCATION:Ens Lyon
END:VEVENT
BEGIN:VEVENT
SUMMARY:Intersection Types and Runtime Errors in the Pi-Calculus - Damiano
Mazza\, CNRS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190221T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190221T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:757
DESCRIPTION:We introduce a type system for the $\\pi$-calculus which is de
signed to guarantee that typable processes are well-behaved\, namely they
never produce a run-time error and\, even if they may diverge\, there is a
lways a chance for them to “finish their work”\, i.e. to reduce to an
idle process. The introduced type system is based on non-idempotent inters
ections\, and is thus very powerful as for the class of processes it can c
apture. Indeed\, despite the fact that the underlying property is $\\Pi^0_
2$-complete\, there is a way to show that the system is complete\, i.e.\,
that any well-behaved process is typable\, although for obvious reasons in
finitely many derivations need to be considered.\n\nJoint work with Ugo Da
l Lago\, Marc De Visme\, Akira Yoshimizu
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Theory of species of structures and applications - François Berge
ron\, UQAM
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190228T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190228T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:767
DESCRIPTION:Species of Structures\, introduced almost 40 years ago\, give
a natural conceptu l framework for the notion of ``combinatorial construct
ion on sets’’. Fundamental operations between species allow the specif
ication of new species in terms of known ones\, giving a systematic contex
t for the solution of classical enumeration questions\, including both lab
elled and unlabelled enumeration (a.k.a. Pólya Theory). In this talk\, we
will give an accessible introduction to the Theory of Species\, with many
illustrations. If time allows\, we will also survey some of many areas (c
omputer science\, theoretical physics\, chemistry\, etc.) where they are c
urrently useful.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Higher Universal Algebra in Dependent Type Theory - Eric Finster\,
Inria - Nantes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190226T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190226T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:808
DESCRIPTION:The naive translation of set-theoretic definitions of algebrai
c\nstructures (such as monoids\, categories and groups) into Martin-Lof\nt
ype theory is often incomplete: without additional hypotheses such as\ntru
ncation or a decidable equality\, these translations fail to specify\nthe
behavior of the structure with respect to higher equalities. On\nthe other
hand\, a complete description of such structures is quite\ndifficult\, as
it typically requires the specification of an infinite\nnumber of equatio
ns. I will present recent progress on this problem\nby giving a definitio
n of a "coherent polynomial monad" internal to\ntype theory.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Quelques résultats sur l'équivalence des preuves dans la logique
linéaire du second ordre - Paolo Pistone\, Univ. Tubingen
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190321T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190321T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:813
DESCRIPTION:Les réseaux de preuves donnent une représentation canonique
des démonstrations dans la logique linéaire multiplicative : l'équivale
nce dénotationnelle des preuves coïncide avec l'équivalence des réseau
x. Par contre\, la canonicité des réseaux ne s'étend pas au second ordr
e. Ce problème est du à la présence des témoins des règles existentie
lles. En fait\, dans plusieurs sémantiques dénotationnelles l'informatio
n portée par les preuves est compressée\, et notamment les témoins exis
tentiels sont effacés.\n\nFont partie de ces sémantiques "effaçantes" l
es sémantiques cohérente et rélationnelle\, ainsi que la sémantique di
naturelle et la sémantique observationnelle. On présente des résultats
sur l'équivalence des preuves dans ces sémantiques et on discute des app
lications en complexité dues à la possibilité de compresser les preuves
.\nUne partie de ces travaux est issue d'une collaboration avec L. Tortora
de Falco\, T. Seiller et L.T.D. Nguyễn.
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:20190319T230300Z
UID:815
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:An application of parallel cut elimination in multiplicative linea
r logic to the Taylor expansion of proof nets - Lionel Vaux\, Amu\, Marsei
lle
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190516T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190516T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:817
DESCRIPTION:We examine some combinatorial properties of parallel cut elimi
nation in\nmultiplicative linear logic (MLL) proof nets. We show that\, pr
ovided we\nimpose a constraint on some paths\, we can bound the size of al
l the nets\nsatisfying this constraint and reducing to a fixed resultant n
et. This\nresult gives a sufficient condition for an infinite weighted sum
of nets\nto reduce into another sum of nets\, while keeping coefficients
finite.\nWe moreover show that our constraints are stable under reduction.
\n\nOur approach is motivated by the quantitative semantics of linear logi
c:\nmany models have been proposed\, whose structure reflect the Taylor\ne
xpansion of multiplicative expo- nential linear logic (MELL) proof nets\ni
nto infinite sums of differential nets. In order to simulate one cut\nelim
ination step in MELL\, it is necessary to reduce an arbitrary number\nof c
uts in the differential nets of its Taylor expansion. It turns out\nour re
sults apply to differential nets\, because their cut elimination is\nessen
tially multiplicative. We moreover show that the set of\ndifferential nets
that occur in the Taylor expansion of an MELL net\nautomatically satisfie
s our constraints.\n\n(Joint work with Jules Chouquet.)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Taylor expansion of probabilistic lambda-terms - Thomas Leventis\,
Univ. Bologna (Italy)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190328T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190328T113000
DTSTAMP;VALUE=DATE-TIME:20190319T230300Z
UID:818
DESCRIPTION:Taylor expansions have been introduced by Ehrhard and Regnier
as a computational interpretation of Girard's quantitative semantics. Lamb
da-terms are expanded into linear combinations of their n-linear approxima
nts\, such approximants being defined as resource lambda-terms. This const
ruction is well-suited to interpret quantitative calculi\, such as the pro
babilistic lambda-calculus: Taylor expansions are linear combinations and
the resource lambda-calculus is linear so interpreting probability distrib
utions over terms is straightforward. Yet paradoxically the proof techniqu
e used by Ehrhard and Regnier to study Taylor expansions heavily rely on t
he particular structure of the expansions of ordinary lambda terms\, and t
hey are not suited to work on a quantitative setting. In this talk we will
show how to indirectly extend their result to probabilistic Taylor expans
ions. First we will introduce explicit Taylor expansions\, which uses "ine
rt" probabilistic choices to interpret probabilistic terms while preservin
g the necessary properties to apply Ehrhard and Regnier's proof techniques
. Then we will show how to extract interesting results on probabilistic Ta
ylor expansions from these explicit Taylor expansions.
LOCATION:Salle 3052
END:VEVENT
END:VCALENDAR