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