Aula 311, Palazzina C, L.go S. Leonardo Murialdo 1
Abstract
One of the main innovations introduced by linear logic at its birth is a representation of proofs as graph-like structures called "proof nets", instead of trees as in natural deductions. However, there have been very few attempts to connect these proof nets with mainstream graph theory. In this talk, we will discuss the benefits of such connections:
- Using a relationship between unique perfect matchings and MLL+Mix proof nets first noticed by Retoré, we obtain the best known algorithms for MLL+Mix correctness and sequentialization, and discover some purely graph-theoretical results inspired by linear logic. (Reference for this part: https://arxiv.org/abs/1901.10247 )
- The notion of combinatorial map (already applied to the combinatorics of the lambda-calculus by Bodini-Gardy-Jacquot, Zeilberger-Giorgetti...) allows us to recast Girard's "long trip" criterion in terms of topology of surfaces, and also induces some clarifications in the theory of cyclic linear logic.
