A Modal Linear Logic for Distribution and Mobility - extended abstract -

Colloque avec actes et comité de lecture. internationale.International audienceWe present a multi-modal, first order, intuitionistic linear logic with locations, called DMLL. It is resource-sensitive and takes into account the notions of location and mobility of formulae (seen as resources) through the introduction of three modalities. We define a sequent calculus for which cut-elimination property is proved, a based-on resource semantic model and thus we prove the soundness and completeness of the calculus. Then, we discuss an extension of DMLL with quantifications over locations, called full-DMLL, and propose, from an appropriate subset, a new distributed process calculus with modalities. The relationships between computations and proof search in such logics will be studied and illustrated in some examples