Differential Interaction Nets and True Concurrency
May 24th 15.00 & May 25th 14.00
Aula C, Palazzo delle Scienze - Cagliari
Laboratoire d'Informatique de Paris Nord, CNRS (France)
Abstract. Differential interaction nets have been introduced by Thomas Ehrhard and Laurent Regnier as an extension of linear logic proof-nets. Their main novelty is the presence of non-determinism in the cut-elimination procedure. This allowed Ehrhard and Laurent to prove that standard process calculi (e.g., pi-calculus, solos calculus) can be encoded into differential nets. However, such techniques exploit an ad-hoc treatment of reduction, which is needed to guarantee the existence of a bisimulation.
In the first part of this talk (May 24th) we will introduce interaction nets, and then differential interaction nets as a special case. In the second part (May 25th), we will analyse differential nets from a "true concurrency" point of view (non-interleaving semantics, in particular based on event structures). We will see that differential nets are inherently less expressive than standard process calculi; we will then see how to enhance their expressivity.