Multiplicative intuitionistic linear logic (MILL) has only multiplicative conjunction $\otimes$ and linear implication $\multimap$ as connectives. It has models in symmetric monoidal closed categories.


Compact closed categories are symmetric monoidal closed categories in which every object $A$ has a dual $A^\*$ and $A \multimap B \cong A^\* \otimes B$. Thought of as a resource, $A^\*$ is a debt, owing someone an $A$. Is there a special name for MILL when these conditions hold? ͏ ͏



What is the proper name for "compact closed" multiplicative intuitionistic linear logic?
This logic was studied by Masaru Shirahata, ["A Sequent Calculus for Compact Closed Categories"](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.3906). He just calls it "CMLL", but points out it is equivalent in provability to MLL (classical multiplicative linear logic) with tensor and par identified. Note that the direction tensor $\vdash$ par is commonly called "MIX", so this is also MLL + MIX as an isomorphism.


