Logic in closed symmetric monoidal categories; reference request. Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models for some commutative algebraic theory, like the equational theory of Abelian groups. Anyway:
Question 0. In what fragment of first-order logic must the axioms for $T$ be specified in order that we may interpret $T$ in any closed symmetric monoidal category? And what inference principles may we use?

I have read that the internal logic of closed monoidal categories is a linear type system. However, I'm not really sure what this means; in fact, I gather its a bit of fluffy statement. From $n$-Lab:

“linear logic” takes on many flavors: in addition to the Girard-style language that is naturally interpreted in star-autonomous categories, one has languages for monoidal biclosed categories, symmetric monoidal closed categories, compact closed categories, and others, collectively representing the “multiplicative” core of linear logic as understood in this general sense.

So what I'd appreciate most would be a reference, somewhere I can get started learning this stuff in a non-fluffy way:
Question 1. Where is a good place to learn about linear type systems in general, and logic in closed symmetric monoidal categories in particular?
 A: I think there is a reference that fits perfectly with your requests (Question 1 and, indirectly, Question 0): 
Paul-André Melliès: Categorical Semantics of Linear Logic. Panoramas et Synthèses 27, Société Mathématique de France, 2009.
This survey is designed to guide the reader in investigating the symbolic mechanisms of cut-elimination in proof theory and especially in linear logic, and their algebraic transcription as coherence diagrams in categories with structure.
From the abstract:

We start the survey by a short introduction to proof theory (Chapter 1)
  followed by an informal explanation of the principles of denotational seman-
  tics (Chapter 2) which we understand as a representation theory for proofs
  – generating algebraic invariants modulo cut-elimination. After describing in
  full detail the cut-elimination procedure of linear logic (Chapter 3), we explain
  how to transcribe it into the language of categories with structure. We review
  three alternative formulations of
  ∗-autonomous category, or monoidal category
  with classical duality (Chapter 4). Then, after giving a 2-categorical account
  of lax and oplax monoidal adjunctions (Chapter 5) and recalling the notions of
  monoids and monads (Chapter 6) we relate four different categorical axiomati-
  zations of propositional linear logic appearing in the literature (Chapter 7). We
  conclude the survey by describing two concrete models of linear logic, based on
  coherence spaces and sequential games (Chapter 8) and by discussing a series
  of future research directions (Chapter 9)

Chapter 4 is devoted to symmetric monoidal closed categories and their relationship with linear logic.
