Sciweavers

MSCS
2007

Proofs, denotational semantics and observational equivalences in Multiplicative Linear Logic

13 years 3 months ago
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.
Michele Pagani
Added 27 Dec 2010
Updated 27 Dec 2010
Type Journal
Year 2007
Where MSCS
Authors Michele Pagani
Comments (0)