Stratified coherence spaces: a denotational semantics for light linear logic

AbstractLight linear logic (LLL) was introduced by Girard as a logical system capturing the class of polytime functions within the proofs-as-programs approach. In the present paper, we undertake a semantical analysis of LLL: a variant of coherence spaces is introduced and we prove that it is a sound model for this system, but not for usual linear logic. A simpler version of the model yields a sound semantics of Elementary linear logic, which is the analog of LLL for the class of Kalmar elementary functions. We illustrate our semantical method by showing how various principles fail in these models