1. Universidade Federal do Rio Grande do Norte
2. Centro de Tecnologia
3. DEB - Departamento de Engenharia Biomédica
4. CT - DEB - Artigos publicados em periódicos

Título:	On concurrent behaviors and focusing in linear logic
Autor(es):	Vega, Carlos Alberto Olarte Pimentel, Elaine Gouvea
Palavras-chave:	Linear logic;Concurrent constraint programming;Proof systems;Focusing;Multi-focusing;Fixed points
Data do documento:	2017
Editor:	Elsevier
Referência:	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
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
URI:	https://repositorio.ufrn.br/jspui/handle/123456789/29725
ISSN:	0304-3975
Aparece nas coleções:	CCET - DM - Artigos publicados em periódicos CT - DEB - Artigos publicados em periódicos

Este item está licenciada sob uma Licença Creative Commons