CITI has stopped operations in 2014, to co-launch NOVA LINCS THIS SITE IS NOT BEING UPDATED SINCE 2013
citi banner
Home Page FCT/UNL UNL
  Home  \  Seminars @ CITI  \  Seminar Page Login  
   
banner bottom
File Top
A General Proof System for Modalities in Concurrent Constraint Programming
{ Wed, 12 Jun 2013, 14h00 }

By: Carlos Olarte  [ show info ]

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)]


Hosted by: Software Systems

Location: DI seminars room

File Bottom