Phase semantics and verification of concurrent constraint programs

Phase semantics and verification of concurrent constraint programs
复制标题

并发约束程序的阶段语义和验证

DOI：
10.1109/lics.1998.705651
复制
发表时间：
1998
期刊：
Proceedings. Thirteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.98CB36226)
影响因子：
--
通讯作者：
S. Soliman
S. Soliman
中科院分区：
--
文献类型：
--
作者：
F. Fages;P. Ruet;S. Soliman

文献摘要

被引文献

相似文献

并发约束程序设计语言的CC类及其基于线性约束系统的非单调扩展LCC类，对于各种可观测量，可以给出吉拉德的直觉线性逻辑的逻辑语义。在本文中，我们解决基本的完整性结果，我们展示了如何阶段语义的线性逻辑可以用来提供简单和非常简洁的“语义”证明GC或LCC程序的安全属性。
The class CC of concurrent constraint programming languages and its non-monotonic extension LCC based on linear constraint systems can be given a logical semantics in Girard's intuitionistic linear logic for a variety of observables. In this paper we settle basic completeness results and we show how the phase semantics of linear logic can be used to provide simple and very concise "semantical" proofs of safety properties for GC or LCC programs.