2 papers
cs.LO2021
Interpreting a concurrent -calculus in differential proof nets (extended version)
Yann Hamdaoui
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. W…
cs.LO2021
An Interactive Proof of Termination for a Concurrent -calculus with References and Explicit Substitutions
Yann Hamdaoui, Benoît Valiron
In this paper we introduce a typed, concurrent -calculus with references featuring explicit substitutions for variables and references. Alongside usual safety properties, we rec…