Functional interpretations of intuitionistic linear logic

Abstract

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. © 2009 Springer Berlin Heidelberg.