On differential interaction nets and the pi-calculus
Résumé
We propose a translation of a finitary (that is, replication-free) version of the pi-calculus into promotion-free differential interaction net structures, a linear logic version of the differential lambda-calculus (or, more precisely, of a resource lambda-calculus). For the sake of simplicity only, we restrict our attention to a monadic version of the pi-calculus, so that the differential interaction net structures we consider need only to have exponential cells. We prove that the nets obtained by this translation satisfy an acyclicity criterion weaker than the standard Girard (or Danos-Regnier) acyclicity criterion, and we compare the operational semantics of the pi-calculus, presented by means of an environment machine, and the reduction of differential interaction nets. Differential interaction net structures being of a logical nature, this work provides a Curry-Howard interpretation of processes.
Loading...