> Interesting, in a class on sub-structural they used / and \ for ordered implication/closure.

A closed monoidal poset that happens to be lattice is called [*residuated lattice*](https://en.wikipedia.org/wiki/Residuated_lattice#Definition).

Some textbooks (and Wikipedia) denote \\(x \multimap z\\) with \\(x / z\\) and call it the *right residual of \\(z\\) by \\(x\\)*. Dually they denote \\(z ⟜ y\\) as the *left residual of \\(z\\) by \\(y\\)* and it is denoted with \\(z \backslash y\\).

The "lollipop" \\(\multimap\\) was, AFAIK, introduced by Jean-Yves Girard in [*Linear Logic* (1987)](https://www.sciencedirect.com/science/article/pii/0304397587900454). Just as fragments of intuitionistic logic can be given semantics in *Cartesian Closed Categories* (CCC)s, the \\(\otimes,\multimap\\)-fragement of linear logic can be given semantics in *Symmetric Monoidal Closed Categories* (SMCCs). There is a nice discussion of this in [*Introduction to Categories and Categorical Logic (2011)*](https://arxiv.org/pdf/1102.1313.pdf) by Abramsky and Tzevelekos.

A closed monoidal poset that happens to be lattice is called [*residuated lattice*](https://en.wikipedia.org/wiki/Residuated_lattice#Definition).

Some textbooks (and Wikipedia) denote \\(x \multimap z\\) with \\(x / z\\) and call it the *right residual of \\(z\\) by \\(x\\)*. Dually they denote \\(z ⟜ y\\) as the *left residual of \\(z\\) by \\(y\\)* and it is denoted with \\(z \backslash y\\).

The "lollipop" \\(\multimap\\) was, AFAIK, introduced by Jean-Yves Girard in [*Linear Logic* (1987)](https://www.sciencedirect.com/science/article/pii/0304397587900454). Just as fragments of intuitionistic logic can be given semantics in *Cartesian Closed Categories* (CCC)s, the \\(\otimes,\multimap\\)-fragement of linear logic can be given semantics in *Symmetric Monoidal Closed Categories* (SMCCs). There is a nice discussion of this in [*Introduction to Categories and Categorical Logic (2011)*](https://arxiv.org/pdf/1102.1313.pdf) by Abramsky and Tzevelekos.