2006
Michele Pagani
To appear in: Mathematical Structures in Computer Science
Abstract
We study full completeness and syntactical separability of M LL proof nets with the mix rule. The general method we use consists ï¬rst 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 ï¬nd a semantical characterization of their interpretations in relational semantics, and we deï¬ne 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 | sepMLL.ps
BibTeX