BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//6.4.7.3//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:7670@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris;VALUE=DATE:20221020
DTEND;TZID=Europe/Paris;VALUE=DATE:20221021
DTSTAMP:20221017T152506Z
URL:https://www.i2m.univ-amu.fr/events/rencontre-chocola-a-lyon/
SUMMARY:Rencontre Chocola à Lyon -
DESCRIPTION:Voir https://chocola.ens-lyon.fr/events/meeting-2022-10-20/ .\n
\n \;\n\nRencontre\, 20 October 2022 \n\n\nWe will be in Amphi B\, 3r
d floor\, Monod site of the ENSL.\n\n\nProgramme\n\n 10:30 – 12:00\n \
nMarie Fortin (IRIF\, CNRS)\n Invited talk: FO = FO^3 for Linear Orders w
ith Monotone Binary Relations\n\n\nIt is well-known that linear orders hav
e the 3-variable property\, meaning that over linear orders\, every monadi
c first-order formula with up to 3 free variables is equivalent to one tha
t uses at most 3 variables in total. This is usually shown through Ehrenfe
ucht–Fraïssé games\, or as a corollary of the expressive completeness
of linear temporal logic (with Stavi connectives). Over the years\, this h
as been extended to richer classes of structures\, such as the real line w
ith the +1 relation\, Mazurkiewicz traces\, or message sequence charts. In
this talk\, I will present a unifying proof that generalizes those facts.
It is based on star-free PDL\, a variant of propositional dynamic logic t
hat is closely related to Tarski’s calculus of relations and captures pr
ecisely the 3-variable fragment of first-order logic. More precisely\, I w
ill show that over structures consisting of one linear order and arbitrari
ly many binary relations satisfying some monotonicity conditions\, star-fr
ee PDL has the same expressive power as full first-order logic. This impli
es that any class of such structures has the 3-variable property.\n\n\n 1
4:00 – 15:00\n \nMartin Baillon (Gallinette\, LS2N)\n Invited talk: Ga
rdening with the Pythia\, A model of continuity in a dependent setting\n\n
\nWe generalize to a rich dependent type theory a proof originally develop
ed by Escardó that all System T functionals are continuous. It relies on
the definition of a syntactic model of Baclofen Type Theory\, a type theor
y where dependent elimination must be strict\, into the Calculus of Induct
ive Constructions.\n\nThe model is given by three translations: the axiom
translation\, that adds an oracle to the context\; the branching translati
on\, based on the dialogue monad\, turning every type into a tree\; and fi
nally\, a layer of algebraic binary parametricity\, binding together the t
wo translations. In the resulting type theory\, every function f : (N →
N) → N is externally continuous.\n\n\n 15:30 – 16:30\n \nTito Nguy
ễn (LIP\, ENS de Lyon)\n Invited talk: A transducer model for simply ty
ped λ-definable functions\n\n\nAmong the natural ways to define functions
ℕ^k → ℕ in the simply typed λ-calculus\, one of them allows hypere
xponential growth (any tower of exponentials) but excludes many basic func
tions such as subtraction and equality\, as was discovered by Statman in t
he 1980s. Until now\, this function class did not have any characterizatio
n not mentioning the λ-calculus. We provide the first one\, which more ge
nerally encompasses λ-definable tree-to-tree functions\, using an automat
a model: "collapsible pushdown transducers". As the name of our machines s
uggests\, we draw on the known connections between collapsible pushdown au
tomata and simply typed λ-calculus with fixpoints\; in fact\, one might t
hink of our results as being about recursion schemes parameterized by fini
te input trees. Other significant inspirations include:\n\n Engelfriet et
al.'s work on higher-order pushdown tree transducers\, which are included
in our model while already being to our knowledge the most expressive tra
nsducer model in the literature (polyregular functions\, macro tree transd
ucers\, etc. define strict subclasses)\;\n an old result of Plotkin\, rec
ently made available thanks to Urzyczyn\n\n(https://arxiv.org/abs/2206.084
13)\, showing that the presence of fixpoints does not affect what total fu
nctions can be expressed.\n\nThis (unpublished) work is a sequel to my col
laboration with Pierre Pradic (Swansea University) on "implicit automata".
\n\nNDLR: the talk will be given on the blackboard\, so it might be not so
easy to follow at a distance\, given the available technology\n\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
022/08/image_aglr-ldp-logo_chocola.png
CATEGORIES:Séminaire Logique et Interactions
LOCATION:ENSL - École normale supérieure de Lyon\, 15 parvis René Descar
tes\, Lyon\, France\, 69342\, France
X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=15 parvis René Descartes\,
Lyon\, France\, 69342\, France;X-APPLE-RADIUS=100;X-TITLE=ENSL - École n
ormale supérieure de Lyon:geo:0,0
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20220327T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR