Interpreting a concurrent $\lambda$-calculus in differential proof nets (extended version)
Logic in Computer Science
2021-02-12 v1
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.
Cite
@article{arxiv.2102.05736,
title = {Interpreting a concurrent $\lambda$-calculus in differential proof nets (extended version)},
author = {Yann Hamdaoui},
journal= {arXiv preprint arXiv:2102.05736},
year = {2021}
}