On concurrent behaviors and focusing in linear logic

Vega, Carlos Alberto Olarte; Pimentel, Elaine Gouvea

On concurrent behaviors and focusing in linear logic

Página do item simplificado Estatísticas

dc.contributor.author	Vega, Carlos Alberto Olarte
dc.contributor.author	Pimentel, Elaine Gouvea
dc.date.accessioned	2020-07-24T18:59:18Z
dc.date.available	2020-07-24T18:59:18Z
dc.date.issued	2017
dc.description.resumo	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	pt_BR
dc.identifier.citation	OLARTE, C.; PIMENTEL, E.. On concurrent behaviors and focusing in linear logic.Theoretical Computer Science, v. 685, p. 46-64, 2017. Disponível em: https://www.sciencedirect.com/science/article/pii/S0304397516304832?via%3Dihub. Acesso em: 21 jul. 2020. https://doi.org/10.1016/j.tcs.2016.08.026	pt_BR
dc.identifier.doi	10.1016/j.tcs.2016.08.026
dc.identifier.issn	0304-3975
dc.identifier.uri	https://repositorio.ufrn.br/jspui/handle/123456789/29725
dc.language	en	pt_BR
dc.publisher	Elsevier	pt_BR
dc.rights	Attribution 3.0 Brazil	*
dc.rights.uri	http://creativecommons.org/licenses/by/3.0/br/	*
dc.subject	Linear logic	pt_BR
dc.subject	Concurrent constraint programming	pt_BR
dc.subject	Proof systems	pt_BR
dc.subject	Focusing	pt_BR
dc.subject	Multi-focusing	pt_BR
dc.subject	Fixed points	pt_BR
dc.title	On concurrent behaviors and focusing in linear logic	pt_BR
dc.type	article	pt_BR