A Proof-theoretic Semantics for Intuitionistic Linear Logic

The approach to giving a proof-theoretic semantics for IMLL taken by Gheorghiu, Gu and Pym is an interesting adaptation of the work presented by Sandqvist in his 2015 paper for IPL. What is particularly interesting is how naturally the move to the substructural setting provided a semantics for the multiplicative fragment of intuitionistic linear logic. Whilst ultimately the authors of the semantics for IMLL used their foundations to provide a semantics for bunched implication logic, it begs the question, what of the rest of intuitionistic linear logic? In this paper, I present a semantics for intuitionistic linear logic, by first presenting a semantics for the multiplicative and additive fragment after which we focus solely on considering the modality "of-course", thus giving a proof-theoretic semantics for intuitionistic linear logic.