Proofs, Denotational Semantics and Observational Equivalences in Multiplicative Linear Logic


Michele Pagani

To appear in: Mathematical Structures in Computer Science


We study full completeness and syntactical separability of M LL 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.

Download: sepMLL.pdf |