The exponential modalities are where infinity resides in propositional linear logic: in the propositional fragments of linear logic without exponential modalities, in some sense 'everything is known in advance', so everything terminates, everything is decidable, etc. Interestingly, it turns out that the usual exponential modalities, which Girard has sometimes referred to as 'orthodox', are not the only possible way of introducing infinity in linear logic: 'heterodox' exponential modalities exist, with quite different structures with respect to the orthodox one. In many cases, these alternative ways of introducing infinity have interesting properties, especially in terms of computational complexity, which we will survey in this talk.[-]

Gentzen's sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut-elimination and consistency for classical and intuitionistic logics. Among the undesirable features of sequent calculi is the fact that their inferences rules are very low-level. We present the focused proof system LKF in which synthetic inference rules can systematically be defined and for which cut-eliminate hold.[-]