Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4951978 | Theoretical Computer Science | 2017 | 24 Pages |
Abstract
In this work we present the focused proof system SELLFâ, which extends intuitionistic linear logic with subexponentials with the ability of quantifying over them, hence allowing for the use of an arbitrary number of modalities. We show that the view of subexponentials as specific modalities is 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 capturing time, spatial and epistemic behaviors into SELLFâ, thus providing a proof theoretic foundation for those calculi and, at the same time, setting SELLFâ as a general framework for specifying such systems.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Vivek Nigam, Carlos Olarte, Elaine Pimentel,