A new correctness criterion for MLL proof nets

ABSTRACT. In Girard's original presentation, proof structures of Linear Logic are hypergraphs whose hyperedges are labeld by logical rules and vertices represent the connections between these logical rules. Presentations of proof structures based on interaction nets have the same kind of graphical flavour. Other presentations of proof structures use terms instead of graphs or hypergraphs. The atomic ingredient of these terms are variables related by axiom links. However, the correctness criteria developped so far are adapted to the graphical presentations of proof structures and not to their term-based presentations. We propose a new correctnes criterion for constant-free Multiplicative Linear Logic with Mix which applies to a coherence space structure that a term-based proof structure induces on the set of its variables in a straightforward way.