@inproceedings{2cf84ccb84a84e259d3ba8eda66de25f,
title = "The separation theorem for differential interaction nets",
abstract = "Differential interaction nets (DIN) have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. We prove that DIN enjoy an internal separation property: given two different normal nets, there exists a dual net separating them, in analogy with B{\"o}hm's theorem for the λ-calculus. Our result implies in particular the faithfulness of every non-trivial denotational model of DIN (such as Ehrhard's finiteness spaces). We also observe that internal separation does not hold for linear logic proof-nets: our work points out that this failure is due to the fundamental asymmetry of linear logic exponential modalities, which are instead completely symmetric in DIN.",
keywords = "Differential interaction nets, Faithfulness, Linear logic, Obser-vational equivalence, Proof-nets",
author = "Damiano Mazza and Michele Pagani",
year = "2007",
month = jan,
day = "1",
doi = "10.1007/978-3-540-75560-9\_29",
language = "English",
isbn = "9783540755586",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "393--407",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 14th International Conference, LPAR 2007, Proceedings",
note = "14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2007 ; Conference date: 15-10-2007 Through 19-10-2007",
}