Proof theory of biproducts? A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts?

Perhaps the best-known example is the category of vector spaces, in which the direct sum and direct product constructions give the same vector space. This means vector spaces and linear maps are a slightly degenerate model of linear logic, and I am curious what a type theory which accepts this degeneracy would look like.
Samson Abramsky and I wrote a paper about the proof theory of compact categories with biproducts.


  Abramsky, S. and Duncan, R. (2006) "A Categorical Quantum Logic",
  Mathematical Structures in Computer Science 16 (3).
  10.1017/S0960129506005275


The ideas were later developed a bit further in this book chapter:


  Duncan, Ross (2010) "Generalised Proof-Nets for Compact Categories
  with Biproducts" in Semantic Techniques in Quantum Computation,
  Cambridge University Press, pp70--134 arXiv:0903.5154v1


The full details are there, but the short version is that your logic is inconsistent, because you have a zero proof for every implication, and the rest of your proofs are equivalent to "matrices", where the matrix entries are the proofs in the biproduct-free part of the logic.  Speaking without the caveats required to make this precise, the resulting category of proofs is the free biproduct category on some category of axioms.