CCET - DM - Artigos publicados em periódicos

URI Permanente para esta coleçãohttps://repositorio.ufrn.br/handle/1/2985

Navegar

Agora exibindo 1 - 2 de 2

On concurrent behaviors and focusing in linear logic
(Elsevier, 2017) Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea
Concurrent Constraint Programming (CCP) is a simple and powerful model of concurrency where processes interact by telling and asking constraints into a global store of partial information. Since its inception, CCP has been endowed with declarative semantics where processes are interpreted as formulas in a given logic. This allows for the use of logical machinery to reason about the behavior of programs and to prove properties of them. Nevertheless, the logical characterization of CCP programs exhibits normally a weak level of adequacy since proofs in the logical system may not correspond directly to traces of the program. In this paper, we study different encodings from CCP into intuitionistic linear logic (ILL) and we compare the level of adequacy attained in each. By relying on a focusing discipline, we show that it is possible to give a logical characterization to CCP with the highest level of adequacy. Moreover, we show how to characterize maximal-parallelism semantics for CCP by relying on a multi-focusing discipline for ILL. These results, besides giving proof techniques for CCP, entail (safe) optimizations for the execution of CCP programs. Finally, we show how to interpret CCP procedure calls as fixed points in ILL, thus opening the possibility of reasoning by induction about properties of CCP programs
Subexponential concurrent constraint programming
(Elsevier, 2015) Pimentel, Elaine Gouvea; Nigam, Vivek; Vega, Carlos Alberto Olarte
In previous works we have shown that linear logic with subexponentials (SELL), a refinement of linear logic, can be used to specify emergent features of concurrent constraint programming (CCP) languages, such as preferences and spatial, epistemic and temporal modalities. In order to do so, we introduced a number of extensions to SELL, such as subexponential quantifiers for the specification of modalities, and more elaborated subexponential structures for the specification of preferences. These results provided clear proof theoretic foundations to existing systems. This paper goes in the opposite direction, answering positively the question: can the proof theory of linear logic with subexponentials contribute to the development of new CCP languages? We propose a CCP language with the following powerful features: 1) computational spaces where agents can tell and ask preferences (soft-constraints); 2) systems where spatial and temporal modalities can be combined; 3) shared spaces for communication that can be dynamically established; and 4) systems that can dynamically create nested spaces. In order to provide the proof theoretic foundations for such a language, we propose a unified logical framework (SELLS) combining the extensions of linear logic with subexponentials mentioned above, and showing that this new framework has interesting proof theoretical properties such as cut-elimination and a sound and complete focused proof system

SIGAA

Navegar

Navegando CCET - DM - Artigos publicados em periódicos por Assunto "Concurrent constraint programming"