Skip to main content
Source Link

Models of intuitionistic linear logic that reflect the resource interpretation

I am interested in models of intuitionistic linear logic, that is, the logic that you get if you take classical linear logic and restrict the set of operators to $\otimes$, $1$, $\multimap$, $\times$, $\top$, $+$, $0$, and $!$. I know what categorical models of this logic are. However I am looking for something more concrete, something that reflects the interpretation that intuitionistic linear logic is about resources.

Intuitionistic linear logic corresponds to a variant of the λ-calculus that cannot only deal with values (which can be duplicated and destroyed at will), but also with resources (which can neither be duplicated nor destroyed by default). The ordinary simply typed λ-calculus can be given a semantics where the meaning of a type is the set of its inhabitants. Can something similar be done for the linear λ-calculus such that the idea of computing with resources is directly expressed?