Please use this identifier to cite or link to this item:
Title: Proving concurrent constraint programming correct, revisited
Authors: Vega, Carlos Alberto Olarte
Pimentel, Elaine Gouvea
Keywords: Linear logic;Concurrent Constraint Programming;Proof Systems;Focusing;Fixed Points
Issue Date: 2015
Publisher: Elsevier
Citation: OLARTE, Carlos; PIMENTEL, Elaine. Proving Concurrent Constraint Programming Correct, Revisited. Electronic Notes In Theoretical Computer Science, [S.L.], v. 312, p. 179-195, abr. 2015. Disponível em: Acesso em: 29 jul. 2020.
Portuguese Abstract: 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 in a declarative way. 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, relying on a focusing discipline, we show that it is possible to give a logical characterization to different CCP-based languages with the highest level of adequacy. We shall also provide a neater way of interpreting procedure calls by adding fixed points to the logical structure
ISSN: 1571-0661
Appears in Collections:CCET - DM - Artigos publicados em periódicos
ECT - Artigos publicados em periódicos

Files in This Item:
File Description SizeFormat 
ProvingConcurrentConstraint_VEGA_2015.pdf279,5 kBAdobe PDFThumbnail

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.