Interpreting a concurrent $\lambda$-calculus in differential proof nets (extended version)

TL;DR

This paper presents a novel interpretation of a concurrent lambda calculus with references and replication into differential proof nets, establishing a formal correspondence and introducing routing areas for communication primitives.

Contribution

It introduces a new translation of a concurrent lambda calculus into differential proof nets, including the novel concept of routing areas for communication.

Findings

Proves a simulation and adequacy theorem for the translation

Defines and studies routing areas as nets for communication primitives

Establishes a formal correspondence between the language and proof nets

Abstract

In this paper, we show how to interpret a language featuring concurrency, references and replication into proof nets, which correspond to a fragment of differential linear logic. We prove a simulation and adequacy theorem. A key element in our translation are routing areas, a family of nets used to implement communication primitives which we define and study in detail.