BEGIN:VCALENDAR VERSION:2.0 PRODID:-//wp-events-plugin.com//7.2.3.1//EN TZID:Europe/Paris X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:5910@i2m.univ-amu.fr DTSTART;TZID=Europe/Paris;VALUE=DATE:20221020 DTEND;TZID=Europe/Paris;VALUE=DATE:20221021 DTSTAMP:20241120T200654Z URL:https://www.i2m.univ-amu.fr/evenements/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\, 3rd 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 Order s with Monotone Binary Relations\n\n\nIt is well-known that linear orders have the 3-variable property\, meaning that over linear orders\, every mon adic first-order formula with up to 3 free variables is equivalent to one that uses at most 3 variables in total. This is usually shown through Ehre nfeucht–Fraïssé games\, or as a corollary of the expressive completene ss of linear temporal logic (with Stavi connectives). Over the years\, thi s has been extended to richer classes of structures\, such as the real lin e with the +1 relation\, Mazurkiewicz traces\, or message sequence charts. In this talk\, I will present a unifying proof that generalizes those fac ts. It is based on star-free PDL\, a variant of propositional dynamic logi c that is closely related to Tarski’s calculus of relations and captures precisely the 3-variable fragment of first-order logic. More precisely\, I will show that over structures consisting of one linear order and arbitr arily many binary relations satisfying some monotonicity conditions\, star -free PDL has the same expressive power as full first-order logic. This im plies that any class of such structures has the 3-variable property.\n\n\n 14:00 – 15:00\n \nMartin Baillon (Gallinette\, LS2N)\n Invited talk: Gardening with the Pythia\, A model of continuity in a dependent setting\ n\n\nWe generalize to a rich dependent type theory a proof originally deve loped by Escardó that all System T functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory\, a type th eory where dependent elimination must be strict\, into the Calculus of Ind uctive Constructions.\n\nThe model is given by three translations: the axi om translation\, that adds an oracle to the context\; the branching transl ation\, based on the dialogue monad\, turning every type into a tree\; and finally\, a layer of algebraic binary parametricity\, binding together th e two translations. In the resulting type theory\, every function f : (N → N) → N is externally continuous.\n\n\n 15:30 – 16:30\n \nTito Ng uyễn (LIP\, ENS de Lyon)\n Invited talk: A transducer model for simply typed λ-definable functions\n\n\nAmong the natural ways to define functio ns ℕ^k → ℕ in the simply typed λ-calculus\, one of them allows hype rexponential growth (any tower of exponentials) but excludes many basic fu nctions such as subtraction and equality\, as was discovered by Statman in the 1980s. Until now\, this function class did not have any characterizat ion not mentioning the λ-calculus. We provide the first one\, which more generally encompasses λ-definable tree-to-tree functions\, using an autom ata model: "collapsible pushdown transducers". As the name of our machines suggests\, we draw on the known connections between collapsible pushdown automata and simply typed λ-calculus with fixpoints\; in fact\, one might think of our results as being about recursion schemes parameterized by fi nite input trees. Other significant inspirations include:\n\n Engelfriet et al.'s work on higher-order pushdown tree transducers\, which are includ ed in our model while already being to our knowledge the most expressive t ransducer model in the literature (polyregular functions\, macro tree tran sducers\, etc. define strict subclasses)\;\n an old result of Plotkin\, r ecently made available thanks to Urzyczyn\n\n(https://arxiv.org/abs/2206.0 8413)\, showing that the presence of fixpoints does not affect what total functions can be expressed.\n\nThis (unpublished) work is a sequel to my c ollaboration 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