TY - GEN
T1 - Phase semantics and verification of concurrent constraint programs
AU - Fages, François
AU - Ruet, Paul
AU - Soliman, Sylvain
N1 - Publisher Copyright:
© 1998 IEEE.
PY - 1998/1/1
Y1 - 1998/1/1
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84902500281
U2 - 10.1109/LICS.1998.705651
DO - 10.1109/LICS.1998.705651
M3 - Conference contribution
AN - SCOPUS:84902500281
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 141
EP - 152
BT - Proceedings - 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998
Y2 - 21 June 1998 through 24 June 1998
ER -