On differential interaction nets and the pi-calculus

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.

Data and Resources

Additional Info

Field Value
Source https://hal.science/hal-00096280
Author Ehrhard, Thomas, Laurent, Olivier
Maintainer CCSD
Last Updated May 5, 2026, 22:42 (UTC)
Created May 5, 2026, 22:42 (UTC)
Identifier hal-00096280
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Preuves, Programmes et Systèmes (PPS) ; Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)
creator Ehrhard, Thomas
date 2006-09-19T00:00:00
harvest_object_id 95a4913c-b2d6-4f0d-bde2-dd10e3828be5
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2024-04-22T00:00:00
set_spec type:UNDEFINED