Abstract : 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.

Keywords : logique linéaire; théorie de la démonstration; complexité algorithmique implicite