Stratified coherence spaces: A denotational semantics for light linear logic (Q1827389): Difference between revisions

The author provides a denotational model for Light Linear Logic, a weak variant of Linear Logic. The model is the category {\text {BSCOH}} of stratified measured coherent spaces (and locally bounded stratified cliques), which is considered to be a sub-category of stratified coherent spaces which is proved to be a model of Elementary Linear Logic (the analogue of Light Linear Logic for the Kalmar elementary functions). The soundness of the model with respect to Light Linear Logic is proved via proof-nets. The model {\text {BSCOH}} is not complete with respect to Light Linear Logic as it validates some extra principles; though it does not satisfy some specific principles (e.g. the iteration principle) which are included in Linear Logic but excluded in Light Linear Logic.