Rencontre, 12 octobre 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 2-gé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 bi-catégorie des bimodules entre opérades symétriques est cartésienne fermée (Fiore-Gambino-Hyland-Wynskel, Gambino-Joyal). Ce résultat signifie essentiellement que le 2-sché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 well-known 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 cut-elimination/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 type-theoretic proof of the Cook-Levin theorem (the result stating that SAT is NP-complete).
