Rencontre, Oct. 12, 2017
La rencontre aura lieu en amphi B.
Programme
 10:30 – 12:00

André Joyal (Univ. Québec à Montréal)Invited talk: Opérades et 2géométrie algébrique
Plusieurs notions de base de l'algèbre commutative et de la géométrie algébrique ont un analogue en théorie des catégories. Ces analogies sont utiles pour comprendre certains résultats de la théorie des opérades. Par exemple, on sait que la bicatégorie des bimodules entre opérades symétriques est cartésienne fermée (FioreGambinoHylandWynskel, GambinoJoyal). Ce résultat signifie essentiellement que le 2schéma associé à une opérade est exponentiable.
 14:00 – 15:00

Luc Pellissier (ENS de Lyon)
General (intuitionistic or classical) proofs can be approximated arbitrarily well by linear proofs, that is, proofs that use each of their premises exactly once. In this work, we show that such linear approximations give rise, through an adapted Grothendieck construction, to intersection type systems for any logical system that can be embed meaningfully into linear logic.
We recover in this way all wellknown intersection type systems, capturing different notions of normalization for various languages, and give a blueprint to compute new ones.
Joint work with Damiano Mazza and Pierre Vial.
 15:30 – 16:30

Damiano Mazza (CNRS, LIPN)Invited talk: A Tour Around Polyadic Approximations
The notion of polyadic approximation originates in Girard's very first paper on linear logic, where it is proved that intuitionistic (and classical) theorems may be approximated arbitrarly well by purely linear theorems, i.e., theorems in what is technically called multiplicative additive linear logic (or the internal language of symmetric monoidal closed categories with finite products and coproducts). We will expore the consequences of taking this idea seriously, in particular extending it all the way up to cutelimination/computation sequences (rather than just formulas/types or proofs/programs). The resulting theory, which is developed in the context of higher multicategories, is quite rich and has far reaching applications, inspiring in particular a typetheoretic proof of the CookLevin theorem (the result stating that SAT is NPcomplete).