Title :
Phase semantics and verification of concurrent constraint programs
Author :
Fages, Francois ; Ruet, Paul ; Soliman, Sylvain
Author_Institution :
LIENS, Ecole Normale Superieure, Paris, France
Abstract :
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
Keywords :
formal logic; logic programming; completeness results; concurrent constraint programming languages; intuitionistic linear logic; linear constraint systems; logical semantics; non-monotonic extension; phase semantics; safety properties; Calculus; Computational modeling; Computer languages; Concurrent computing; Linear programming; Logic programming; Propagation delay; Protocols; Safety; Search problems;
Conference_Titel :
Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on
Conference_Location :
Indianapolis, IN
Print_ISBN :
0-8186-8506-9
DOI :
10.1109/LICS.1998.705651
