The separation property for differential interaction nets

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 Bohm’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