Using linear logic in algebraic geometry and commutative algebra In algebraic geometry and commutative algebra we often deal with many categories that are not topoi nor cartesian closed (or even locally CC), but are nevertheless closed monoidal. These include the category $\mathbf{Mod}_R$ of modules over a commutative ring $R$, the category $\mathbf{PShMod}_X$ of presheaves of modules over a scheme $X$ (perhaps also $\mathbf{ShMod}_X$?), and et cetera.
Of course, there are a lot of topoi occuring in algebraic geometry, but others are not. If a category is not a topos, one can't use "normal" intuitionistic reasoning inside the category (because its internal logic does not entail higher-order intuitionistic logic, or the Calculus of Constructions from a TCS point-of-view). Then, as a computer scientist, the natural idea would be: since the internal logic of a monoidal category is some form of linear logic, can we use linear logic fruitfully to study those categories, perhaps in the style of Blechschmidt?
I found this recent manuscript by Paul-André Melliès, which was apparently submitted to LICS 2020 but not accepted. I can't find anything else in this direction, so is this a problem that has been considered in the past? Does anyone have any pointers in this direction and/or perhaps related work? It seems that this has some connections with Tannaka duality, but this is not a topic I'm familiar with at all...
 A: If Simon Henry has not found anything beyond the references you have already mentioned, I doubt very much there is anything out there (though one never knows, math is full of works kept in drawers, or published in some remote journal..).
So, the only option seems to be: let us reason together and see how far we can go. Before I start, let me tell you that your question rocks. I have also to declare that it is a bit loose, and that perhaps by making it a tad more focused we could find the magic thread to answering it.
Your line of thought is:
1.Monoidal closed categories come equipped with (a fragment of) linear logic, so it makes sense to leverage such a logic to describe "things" and "constructions" within those categories.
2.Moreover, you suggest that some cats such as R-MOD (the archetypal monoidal closed cat) and sheaves/presheaves of modules over a scheme are ubiquitous in Algebraic Geometry. Thus, assuming that linear logic tells us something about such cats, perhaps it is also useful to express meaningful procedures in Algebraic Geometry.
Breaking it down in these two steps has an advantage: if we can validate 1, we have some chance to also address 2.
Let us start with 1 then.
What you stated about linear logic basically says: linear logic is kind of the vanilla internal logic for monoidal closed cats (CMC in what follows). Now, as one would expect, this does not tell much as far as specific monoidal cats, only about general constructions and entities living in any generic CMC.
Take for instance the ring R of polynomials over a field (which is exactly the archetypal algebraic structure for classical AG). Now, consider the CMC of its modules.
Can I describe it by a list of linear logic axioms?
In other words, is there a linear theory which is valid in this cat or cats equivalent to it? I do not know the answer, but this is definitely the very first step I would take.
Assume one gets somewhere with 1, and now tries to tackle 2.
Here is what I would do: there is an entire field called Computational Algebraic Geometry, with gadgets like Grobner Basis and the like.

*

*Can one axiomatize these constructions  in the internal linear theory (see previous point) of polynomial rings?*

If that were possible, it would be quite interesting to computer scientists, for instance in that one could develop a sort of "Linear Prolog" to describe computational AG and computational commutative algebra.
There is something else, much bigger than this, but I shall stop here (but see my last question on quantale sub-object classifiers )
One last reference: almost nobody has tried to take seriously Linear Logic as THE logic of constructive math. There are a few refs worth while though, one being Mike Shulman's article here
