From Ordered Monoids to Quantales and Petri Nets: Revised Semantics and Completeness Results in Intuitionistic Linear Logic

Submitted to a Journal. Rapport interne.In this paper, in contrast with previous proof-theoretic studies, we aim to analyse some foundations of frameworks based on linear logic (LL), but from a semantical point of view. We propose at first to revise the semantics of Intuitionistic Linear Logic (ILL), starting with an unified analysis of known semantics of ILL, like phase semantics or Petri nets semantics. We study the embedding of ordered monoids into quantales from the relationships between the notions of order and closure, and then we obtain general constructions and results about such embedding. It naturally leads to a new semantics based on ordered monoid that is complete for the full fragment of ILL. Moreover, we analyse the relationships between ordered monoids and Petri nets and deduce, from the previous results, a completeness result for a new Petri net semantics of ILL. Finally, we show how it is possible to consider a similar approach for the non-commutative ILL