On concurrent behaviors and focusing in linear logic

dc.contributor.authorVega, Carlos Alberto Olarte
dc.contributor.authorPimentel, Elaine Gouvea
dc.date.accessioned2020-07-24T18:59:18Z
dc.date.available2020-07-24T18:59:18Z
dc.date.issued2017
dc.description.resumoConcurrent 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 programspt_BR
dc.identifier.citationOLARTE, 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.026pt_BR
dc.identifier.doi10.1016/j.tcs.2016.08.026
dc.identifier.issn0304-3975
dc.identifier.urihttps://repositorio.ufrn.br/jspui/handle/123456789/29725
dc.languageenpt_BR
dc.publisherElsevierpt_BR
dc.rightsAttribution 3.0 Brazil*
dc.rights.urihttp://creativecommons.org/licenses/by/3.0/br/*
dc.subjectLinear logicpt_BR
dc.subjectConcurrent constraint programmingpt_BR
dc.subjectProof systemspt_BR
dc.subjectFocusingpt_BR
dc.subjectMulti-focusingpt_BR
dc.subjectFixed pointspt_BR
dc.titleOn concurrent behaviors and focusing in linear logicpt_BR
dc.typearticlept_BR

Arquivos

Pacote Original

Agora exibindo 1 - 1 de 1
Carregando...
Imagem de Miniatura
Nome:
ConcurrentBehaviorsAndFocusing_2017.pdf
Tamanho:
554.84 KB
Formato:
Adobe Portable Document Format
Carregando...
Imagem de Miniatura
Baixar

Licença do Pacote

Agora exibindo 1 - 1 de 1
Nenhuma Miniatura disponível
Nome:
license.txt
Tamanho:
1.45 KB
Formato:
Item-specific license agreed upon to submission
Nenhuma Miniatura disponível
Baixar