The ties between propositional linear logic on the one hand and extensions of vector addition systems on the other hand have long been known, as they lie for instance at the heart of Lincoln et al.'s 1992 undecidability proof. With Ranko Lazić we recently revisited these connections with an eye on complexity issues, which allowed us to prove tight complexity bounds on provability in affine and contractive fragments of linear logic. Our work also yields a new Tower lower bound on provability in MELL, for which decidability is still open.

Work presented at CSL-LICS 2014; full paper available on arXiv: http://arxiv.org/abs/1401.6785.