Recently, I read on the nLab that the category of Banach spaces and linear contractions is small complete, small cocomplete, and monoidal closed.
This means that Banach spaces and short linear maps form a model of intuitionistic multiplicative-additive linear logic, and the fact that it is small (co)complete seems to suggest that the construction of Melliès, Tabareau and Tasson in An explicit formula for the free exponential modality of linear logic would go through in this category, supplying an interpretation of the exponential as well.
I found this quite surprising, since interpreting linear logic in infinite-dimensional vector spaces seems to have prompted an awful lot of work over the last two decades.
Does this model for ILL with an exponential actually work? I haven't seen it before in the literature, so maybe it fails for some obvious reason that I am overlooking...
If so, what is the motivation for placing so much emphasis on finding models of specifically classical linear logic in (some restriction of) infinite-dimensional vector spaces?