vix.ing · top · new · best · stats · spec

Interpreting a concurrent λ-calculus in differential proof nets (extended version)

2021/02/10 by Hamdaoui, Yann
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2102.05736

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.

Related