Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic

We study full completeness and syntactical separability of MLL proof nets with the mix rule. The general method we use consists first in addressing the two questions in the less restrictive framework of proof structures, and then in adapting the results to proof nets. At the level of proof structures, we find a semantical characterization of their interpretations in relational semantics, and we define an observational equivalence which is proved to be the equivalence induced by cut elimination. Hence, we obtain a semantical characterization (in coherent spaces) and an observational equivalence for the proof nets with the mix rule.

• Type: Journal
• Year: 2007
• Where: MSCS
• Authors: Michele Pagani
• Keywords: Mix Rule, MSCS 2007, Proof Structures, Semantical Characterization