DocumentCode
1955027
Title
Phase semantics and verification of concurrent constraint programs
Author
Fages, Francois ; Ruet, Paul ; Soliman, Sylvain
Author_Institution
LIENS, Ecole Normale Superieure, Paris, France
fYear
1998
fDate
21-24 Jun 1998
Firstpage
141
Lastpage
152
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on
Conference_Location
Indianapolis, IN
ISSN
1043-6871
Print_ISBN
0-8186-8506-9
Type
conf
DOI
10.1109/LICS.1998.705651
Filename
705651
Link To Document