On the relation between coherence semantics and multiplicative proof nets

Abstract : It is known that (mix) proof nets admits a coherence semantics, computed as a set of experiments. We prove here the converse: a proof structure is shown to be a proof net whenever its sets of experiments is a semantical object --- a clique of the corresponding coherence space. Moreover the interpretation of atomic formulae can be restricted to a given coherent space with three tokens in its web. This is done by transforming \tt cut links into \tt tensor links. Dealing directly with non-cut-free proof structure we characterise the deadlock freeness of the reduced proof structure. These results are especially convenient for Abramsky's proof expressions, and can be extended to the pomset calculus.