So-called relational semantics of linear logic is usually regarded as a denotational semantics reflecting the resource-sensitiveness of the system.
Every type A is interpreted as a set $[\![A ]\!]$, and every proof $\pi$ of a sequent $\Gamma \vdash A$ is interpreted as a binary relation $[\![\pi]\!] \subseteq [\![\Gamma]\!]\times [\![A]\!]$, where clearly $\times$ denotes the product of sets.
The interpretation is self-dual, in the sense that $[\![A ]\!] = [\![A^{\bot} ]\!]$. Therefore every operator of linear logic is interpreted in the same way as its dual:
- both $\otimes$ and its dual "par" (i.e. the upside-down "$\&$"), and in fact even $\multimap$, are interpreted as the product of sets $\times$;
- both $\&$ and its dual $\oplus$ are interpreted as the disjoint union of sets;
- $T$ is the empty set $\emptyset$ and 1 is the singleton $\{*\}$;
- both $!$ and its dual $?$ are interpreted as the finite multisets operator $\mathcal{M}_f$ (for every set $X$ we call $\mathcal{M}_f(X)$ the set of all finite multisets with elements in X).
From the categorical perspective, this means that the category Rel whose objects are sets and whose morphisms are binary relations - together with all the stuff listed above - is a self-dual $\star$-autonomous category (i.e., a symmetric closed monoidal category with a dualizing object $\bot$) and at the same time a cartesian category. This model has been known as a kind of toy model of linear logic since the discovery of the system in the 80's.
By the co-Kleisli construction of the comonad $! = \mathcal{M}_f\,$ one also gets a CCC, i.e. a categorical model of the simply typed $\lambda$-calculus. This one is "less toy". A term $x_1:A_1,\dots,x_n:A_n \vdash M: A$ is interpreted as a binary relation between the disjoint union of all the $\mathcal{M}_f([\![A_i]\!])$ on one side and the set $[\![A]\!]$ on the other. One can see the idea of resources explicitly represented in this interpretation, because of the multiplicities that elements can have in the multisets interpreting the entries of the program.
The same can be said for the models of the untyped $\lambda$-calculus that one can find therein. The first one appeared at the end of this article:
[Hyland, Nagayama, Power, Rosolini: A Category Theoretic Formulation for Engeler-style Models of the Untyped λ-Calculus. ENTCS 161 (2006)]
Another one - a relational version of Scott's $D_{\infty}$ - was studied in
http://www.pps.univ-paris-diderot.fr/~ehrhard/pub/rellam.pdf
(this paper is also a decent introduction to all the basic technicalities concerning relational semantics)
and its relation to $D_{\infty}$ was further explored in
[Ehrhard: the Scott model of Linear Logic is the extensional collapse of its relational model. TCS 424 (2012)].
A generalization of relational semantics where binary relations (i.e. matrixes with entries 0 and 1) are replaced with matrixes on more general rings is developed in
[Laird, Manzonetto, McCusker, Pagani: Weighted relational models of typed lambda-calculi. LICS'13]
People in Cambridge are also exploring a 2-categorical approach to semantics of linear logic and $\lambda$-calculus inspired by relational semantics, where binary relations are replaced by pro functors, see for instance:
[Hyland: Some reasons for generalising domain theory. MSCS 20 (2010)]
