Mirantão and Linear Dependencies

Mirantão, or actually the `Pensão Renascer' in Mirantão is very pretty.  Rustic, with delicious food, very nice people and landscapes to remind you of a Minas Gerais that only exists in the old songs of Milton Nascimento and Fernando Brant.

But Jornadas Mirantão is not about Club de Esquina nor about the world of Guimarães Rosa, re-inventing o sertão. Jornadas Mirantão are about logic and proof theory in beautiful places. So I talked about an old work with Torben Bra\"u ner that I would like to go back to. This is about using linear dependencies between formulas to describe precisely (and without the support of terms) the system called Full Intuitionistic Linear Logic. The slides are in slideshare and the technical report in Cut-Elimination for Full Intuitionistic Linear Logic. (with Brauner). Technical Report 395 from Computer Laboratory, University of Cambridge and BRICS, Denmark. May 1996.