Orateur
Description
After a short introduction to the functorial approach to logical proofs and programs initiated by Lambek in the late 1960s, based on the notion of free cartesian closed category, we will describe a recent convergence with the notion of ribbon category introduced in 1990 by Reshetikhin and Turaev in their functorial study of quantum groups and knot invariants. The connection between proof theory and knot theory relies on the notion of ribbon dialogue category, defined by relaxing the traditional assumption that duality is involutive in a ribbon category. We will explain first how to construct the free such dialogue category using a logic of tensor and negation inspired by the work by Girard on linear logic. A coherence theorem for ribbon dialogue categories will be then established, which ensures that two tensorial proofs are equal precisely when their underlying ribbon tangles are equivalent modulo deformation. At the end of the talk, we will show how to understand these ribbon tangles as interactive Opponent/Player strategies tracking the flow of negation functors in dialogue games. The resulting diagrammatic description of tensorial proofs as interactive strategies is performed in the 3-dimensional language of string diagrams for monoidal 2-categories (or more generally weak 3-
categories) initiated in the mid 1990s by Street and Verity, McIntyre and Trimble.
A few references:
https://www.irif.fr/ ̃mellies/hdr-mellies.pdf
https://www.irif.fr/ ̃mellies/tensorial-logic/1-game-semantics-in-string-diagrams.pdf
https://www.irif.fr/ ̃mellies/papers/lics2018-ribbon-tensorial-logic.pdf
