We present three functional interpretations of intuitionistic linear logic and show how these correspond to well-known functional interpretations of intuitionistic logic via embeddings of ILω into ILLω. The main difference from previous work of the second author is that in intuitionistic linear logic the interpretations of !A are simpler (at the cost of an asymmetric interpretation of pure ILLω) and simultaneous quantifiers are no longer needed for the characterisation of the interpretations.
['Gilda Ferreira', 'Paulo Oliva']
Functional interpretations of intuitionistic linear logic