检索结果-内蒙古大学图书馆

26th International Conference on Logic programming (ICLP)

作者： Aristizabal P, Andres A. LIX Ecole Polytech CNRS Route Saclay F-91128 Palaiseu France INRIA Team COMETE Route Saclay F-91128 Palaiseu France

ISBN: (纸本)9783939897170

In this doctoral work we aim at developing a new approach to labelled semantics and equivalences for the concurrent constraint programming (CCP) which will enable a broader capture of processes behavioural equivalence. Moreover, we work towards exploiting the strong connection between first order logic and CCP. Something which will allow us to represent logical formulae in terms of CCP processes and verify its logical equivalence by means of our notion of bisimilarity. Finally, following the lines of the Concurrecy Workbench we plan to implement a CCP Workbench based on our theoretical structure.

关键词： concurrent constraint programming Concurrency Behavioural Equivalence Bisimilarity Process Calculi Operational Semantics Labelled Semantics

来源：评论

学校读者我要写书评

暂无评论

Types for Secure Pattern Matching with Local Knowledge in Universal concurrent constraint programming

Types for Secure Pattern Matching with Local Knowledge in Un...

引用

25th International Conference on Logic programming (ICLP)

作者： Hildebrandt, Thomas Lopez, Hugo A. IT Univ Copenhagen Programming Log & Semant Grp DK-2300 Copenhagen S Denmark

ISBN: (纸本)9783642028458

The fundamental primitives of concurrent constraint programming (CCP), tell and ask, respectively adds knowledge to and infers knowledge from a shared constraint store. These features, and the elegant use of the constraint system to represent the abilities of attackers, make concurrent constraint programming and timed CCP (tcc) interesting candidates for modeling and reasoning about security protocols. However, they lack primitives for the communication of secrets (or local names as in the pi -calculus) between agents. The recently proposed universal tcc (utcc) introduces a universally quantified ask operation that makes it possible to infer knowledge which is local to other agents. However, it allows agents to guess knowledge even if it is encrypted or communicated on secret channels, simply by quantifying over both the encryption key (or channel) and the message simultaneously. We present a secure utcc (utcc(s)) based on: (i) a simple type system for constraints allowing to distinguish between restricted (secure) and non-restricted (universally quantifiable) variables in constraints, and (ii) a generalization of the universally quantified ask operation to allow the assumption of local knowledge. We illustrate the use of the utcc(s) calculus with examples on communication of local names (as in the pi -calculus) and for giving semantics to secure pattern matching in a prototypical security language.

关键词： concurrent constraint programming Process Calculi Type systems Mobility Security

来源：评论

学校读者我要写书评

暂无评论

A Proof Theoretic Study of Soft concurrent constraint programming

A Proof Theoretic Study of Soft Concurrent Constraint Progra...

引用

30th International Conference on Logic programming

作者： Pimentel, Elaine Olarte, Carlos Nigam, Vivek Univ Fed Rio Grande do Norte BR-59072970 Natal RN Brazil Pontificia Univ Javeriana Cali Javeriana Colombia Univ Fed Paraiba BR-58059900 Joao Pessoa Paraiba Brazil

concurrent constraint programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic -ILL- and processes can be interpreted as formulas in ILL. constraints as ILL formulas fail to represent accurately situations where "preferences" (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical meaning to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings. This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.

关键词： concurrent constraint programming Linear Logic Soft constraints

来源：评论

学校读者我要写书评

暂无评论

A Symbolic Model for Timed concurrent constraint programming

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2015年 312卷 161-177页

作者： Arias, Jaime Guzman, Michell Olarte, Carlos Univ Bordeaux LaBRI UMR 5800 F-33400 Talence France CNRS LaBRI UMR 5800 F-33400 Talence France Univ Valle DECC Cali Colombia Univ Fed Rio Grande do Norte ECT BR-59072970 Natal RN Brazil Pontificia Univ Javeriana Cali DECC Cali Colombia

concurrent constraint programming (ccp) is a model for concurrency where agents interact with each other by telling and asking constraints (i. e., formulas in logic) into a shared store of partial information. The ntcc calculus extends ccp with the notion of discrete time-units for the specification of reactive systems. Moreover, ntcc features constructors for non-deterministic choices and asynchronous behavior, thus allowing for (1) synchronization of processes via constraint entailment during a time-unit and (2) synchronization of processes along time-intervals. In this paper we develop the techniques needed for the automatic verification of ntcc programs based on symbolic model checking. We show that the internal transition relation, modeling the behavior of processes during a time-unit (1 above), can be symbolically represented by formulas in a suitable fragment of linear time temporal logic. Moreover, by using standard techniques as difference decision diagrams, we provide a compact representation of these constraints. Then, relying on a fixpoint characterization of the timed constructs, we obtain a symbolic model of the observable transition (2 above). We prove that our construction is correct with respect to the operational semantics. Finally, we introduce a prototypical tool implementing our method.

关键词： concurrent constraint programming temporal logic model checking

来源：评论

学校读者我要写书评

暂无评论

On subexponentials, focusing and modalities in concurrent systems

引用

THEORETICAL COMPUTER SCIENCE 2017年 693卷 35-58页

作者： Nigam, Vivek Olarte, Carlos Pimentel, Elaine Univ Fed Paraiba Joao Pessoa Paraiba Brazil Univ Fed Rio Grande do Norte ECT Natal RN Brazil Univ Fed Rio Grande do Norte DMAT Natal RN Brazil Fortiss Munich Germany

In this work we present the focused proof system SELLF(sic), which extends intuitionistic linear logic with subexponentials with the ability of quantifying over them, hence allowing for the use of an arbitrary number of modalities. We show that the view of subexponentials as specific modalities is general enough to give a modular encoding of different flavors of concurrent constraint programming (CCP), a simple and powerful model of concurrency. More precisely, we encode CCP calculi capturing time, spatial and epistemic behaviors into SELLF(sic), thus providing a proof theoretic foundation for those calculi and, at the same time, setting SELLF(sic) as a general framework for specifying such systems. (C) 2017 Elsevier B.V. All rights reserved.

关键词： Linear logic concurrent constraint programming Proof systems

来源：评论

学校读者我要写书评

暂无评论

Dynamic Slicing for concurrent constraint Languages

引用

FUNDAMENTA INFORMATICAE 2020年第3-4期177卷 331-357页

作者： Falaschi, Moreno Gabbrielli, Maurizio Olarte, Carlos Palamidessi, Catuscia Univ Siena Dept Informat Engn & Math Siena Italy Univ Bologna Dipartimento Informat Sci & Ingn Bologna Italy Univ Fed Rio Grande do Norte ECT Escola Ciencias & Tecnol Natal RN Brazil Ecole Polytech INRIA Palaiseau France Ecole Polytech LIX Palaiseau France

concurrent constraint programming (CCP) is a declarative model for concurrency where agents interact by telling and asking constraints (pieces of information) in a shared store. Some previous works have developed (approximated) declarative debuggers for CCP languages. However, the task of debugging concurrent programs remains difficult. In this paper we define a dynamic slicer for CCP (and other language variants) and we show it to be a useful companion tool for the existing debugging techniques. We start with a partial computation (a trace) that shows the presence of bugs. Often, the quantity of information in such a trace is overwhelming, and the user gets easily lost, since she cannot focus on the sources of the bugs. Our slicer allows for marking part of the state of the computation and assists the user to eliminate most of the redundant information in order to highlight the errors. We show that this technique can be tailored to several variants of CCP, such as the timed language nt cc, linear CCP (an extension of CCP-based on linear logic where constraints can be consumed) and some extensions of CCP dealing with epistemic and spatial information. We also develop a prototypical implementation freely available for making experiments.

关键词： concurrent constraint programming Program slicing Debugging

来源：评论

学校读者我要写书评

暂无评论

Transformations of CCP programs

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 2001年第3期23卷 304-395页

作者： Etalle, S Gabbrielli, M Meo, MC Univ Twente Fac Comp Sci NL-7500 AE Enschede Netherlands Univ Bologna Dipartimento Sci Informaz I-40127 Bologna Italy Univ G dAnnunzio Dipartimento Sci I-65127 Pescara Italy

We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations that guarantee the input/output CCP semantics is also preserved when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) nonterminating computations. The system allows us to optimize CCP programs while preserving their intended meaning: In addition to the usual benefits for sequential declarative languages, the transformation of concurrent programs can also lead to the elimination of communication channels and of synchronization points, to the transformation of nondeterministic computations into deterministic ones, and to the crucial saving of computational space. Furthermore, since the transformation system preserves the deadlock behavior of programs, it can be used for proving deadlock-freeness of a given program with respect to a class of queries. To this aim, it is sometimes sufficient to apply our transformations and to specialize the resulting program with respect to the given queries in such a way that the obtained program is trivially deadlock-free.

关键词： languages theory concurrent constraint programming deadlock-freeness optimization

来源：评论

学校读者我要写书评

暂无评论

Observational equivalences for linear logic concurrent constraint languages

引用

THEORY AND PRACTICE OF LOGIC programming 2011年第4-5期11卷 469-485页

作者： Haemmerle, Remy Tech Univ Madrid Madrid Spain

Linear logic concurrent constraint programming (LCC) is an extension of concurrent constraint programming (CC), where the constraint system is based on Girard's linear logic instead of the classical logic. In this paper, we address the problem of program equivalence for this programming framework. For this purpose, we present a structural operational semantics for LCC based on a label transition system and investigate different notions of observational equivalences inspired by the state of art of process algebras. Then, we demonstrate that the asynchronous pi-calculus can be viewed as simple syntactical restrictions of LCC. Finally, we show that LCC observational equivalences can be transposed straightforwardly to classical concurrent constraint languages and constraint Handling Rules, and investigate the resulting equivalences.

关键词： concurrent constraint programming linear logic observational equivalences bisimulation pi-calculus constraint Handling Rules

来源：评论

学校读者我要写书评

暂无评论

Logic programming in the context of multiparadigm programming: the Oz experience

引用

THEORY AND PRACTICE OF LOGIC programming 2003年第6期3卷 717-763页

作者： Van Roy, P Brand, P Duchier, D Haridi, S Schulte, C Henz, M Catholic Univ Louvain B-1348 Louvain Belgium Swedish Inst Comp Sci S-16428 Kista Sweden Univ Saarland D-66123 Saarbrucken Germany Royal Inst Technol KTH S-16428 Kista Sweden Natl Univ Singapore Singapore 117543 Singapore

Oz is a multiparadigm language that supports logic programming as one of its major paradigms. A multiparadigm language is designed to support different programming paradigms (logic, functional, constraint, object-oriented, sequential, concurrent, etc.) with equal ease. This paper has two goals: to give a tutorial of logic programming in Oz;and to show how logic programming fits naturally into the wider context of multiparadigm programming. Our experience shows that there are two classes of problems, which we call algorithmic and search problems, for which logic programming can help formulate practical solutions. Algorithmic problems have known efficient algorithms. Search problems do not have known efficient algorithms but can be solved with search. The Oz support for logic programming targets these two problem classes specifically, using the concepts needed for each. This is in contrast to the Prolog approach, which targets both classes with one set of concepts, which results in less than optimal support for each class. We give examples that can be run interactively on the Mozart system, which implements Oz, To explain the essential difference between algorithmic and search programs, we define the Oz execution model. This model subsumes both concurrent logic programming (committed-choice-style) and search-based logic programming (Prolog-style). Furthermore, as consequences of its multiparadigm nature, the model supports new abilities such as first-class top levels, deep guards, active objects, and sophisticated control of the search process. Instead of Horn clause syntax, Oz has a simple, fully compositional, higher-order syntax that accommodates the abilities of the language. We give a brief history of Oz that traces the development of its main ideas and we summarize the lessons learned from this work. Finally, we give many entry points into the Oz literature.

关键词： multiparadigm programming language design Prolog Oz encapsulated search concurrent constraint programming history software development

来源：评论

学校读者我要写书评

暂无评论

On concurrent behaviors and focusing in linear logic

引用

THEORETICAL COMPUTER SCIENCE 2017年 685卷 46-64页

作者： Olarte, Carlos Pimentel, Elaine Univ Fed Rio Grande do Norte Escola Ciencias & Tecnol Natal RN Brazil Univ Fed Rio Grande do Norte Dept Matemat Natal RN Brazil

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. (C) 2016 Elsevier B.V. All rights reserved.

关键词： Linear logic concurrent constraint programming Proof systems Focusing Multi-focusing Fixed points

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：