ct.category theory - What is the proper name for "compact closed" multiplicative intuitionistic linear logic?

Compact closed categories are models of classical linear logic when tensor and par collapse.

As an aside, I'm not sure that the particular resource interpretation you're suggesting genuinely works, since linear logic offers a unified and very subtle view of action and resource. If you want a pure resource interpretation of logic, you may need to look at bunched implications (ie, at categories which simultaneously have a monoidal and cartesian closed structure).

James Brotherston has investigated a version of this logic which is directly inspired by the debt/credit view, called "classical BI", both model-theoretically and proof-theoretically (though not yet categorically).