Functional Interpretations of Intuitionistic Linear Logic

We present three different functional interpretations of intuitionisticlinear logic ILL and show how these correspond to well-known functionalinterpretations of intuitionistic logic IL via embeddings of IL into ILL. Themain difference from previous work of the second author is that inintuitionistic linear logic (as opposed to classical linear logic) theinterpretations of !A are simpler and simultaneous quantifiers are no longerneeded for the characterisation of the interpretations. We then compare ourapproach in developing these three proof interpretations with the one of dePaiva around the Dialectica category model of linear logic