Detail

A General Proof System for Modalities in Concurrent Constraint Programming

In order to specify the behavior of a concurrent system, one has to
often reason about the epistemic state of agents, or the spatial and
temporal state of the system.

In this work, we propose the proof system SELL as a general framework
for specifying such systems. In particular, it extends linear logic
with subexponentials with the ability of quantifying over
subexponentials. Hence, SELL allows for the use of an arbitrary number
of modalities.

We show that, by giving a proper structure to subexponentials, we can
specify concurrent systems that involve modalities, such as the ones
described above.

The view of subexponentials as specific modalities turns out to be
general enough to give a modular encoding of different flavors of
Concurrent Constraint Programming (CCP), a simple and powerful model
of concurrency.
More precisely, we encode CCP calculi with the ability to represent
time, spatial and epistemic behavior into SELL, thus providing a
proof-theoretic foundation for those calculi.

[Joint work with Vivek Nigam (Universidade Federal da Paraíba) and
Elaine Pimentel (Universidade Federal de Minas Gerais)]