Évènement

Lê Thành Dũng (Tito) Nguyễn
ÉNS Lyon
https://nguyentito.eu/

Date(s) : 05/09/2024   iCal
11h00 - 12h30

Our goal is to generalize a little-known but powerful « bridge theorem » of Engelfriet and Maneth, which can be used for instance to refute in a few pages the main theorem of a LICS’20 paper, cf. https://arxiv.org/abs/2301.09234
This theorem is about the tree-to-string functions computed by safe higher-order transducers. We would like to lift this safety condition (analogous to the one for recursion schemes), i.e. generalize the theorem to transducers involving arbitrary simply-typed λ-terms. In the unsafe setting, the known proof technique – which implicitly involves a linearity argument – fails.
To solve this problem, we are led to some plausible conjectures on a non-standard « semi-quantitative » exponential on coherence spaces, and on a finitary variant of Taylor expansion that only distinguishes between discarded arguments, linear arguments and arguments used at least twice.
This work-in-progress is joint with Paweł Parys (MIMUW, University of Warsaw).

Emplacement
LIS, salle 04.05

Catégories

• Séminaire