Phase semantics and verification of concurrent constraint programs

François Fages; Paul Ruet; Sylvain Soliman

doi:10.1109/LICS.1998.705651

Phase semantics and verification of concurrent constraint programs

François Fages
, Paul Ruet
, Sylvain Soliman

École Polytechnique

Centre national de la recherche scientifique

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Proceedings - 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	141-152
Number of pages	12
ISBN (Electronic)	0818685069
DOIs	https://doi.org/10.1109/LICS.1998.705651
Publication status	Published - 1 Jan 1998
Event	13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998 - Indianapolis, United States Duration: 21 Jun 1998 → 24 Jun 1998

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
Volume	1998-June
ISSN (Print)	1043-6871

Conference

Conference	13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998
Country/Territory	United States
City	Indianapolis
Period	21/06/98 → 24/06/98

Access to Document

10.1109/LICS.1998.705651

Cite this

Fages, F., Ruet, P., & Soliman, S. (1998). Phase semantics and verification of concurrent constraint programs. In Proceedings - 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998 (pp. 141-152). (Proceedings - Symposium on Logic in Computer Science; Vol. 1998-June). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/LICS.1998.705651

@inproceedings{a3cc27106c8f4a888a6dc64abd42e8ee,

title = "Phase semantics and verification of concurrent constraint programs",

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.",

author = "Fran{\c c}ois Fages and Paul Ruet and Sylvain Soliman",

note = "Publisher Copyright: {\textcopyright} 1998 IEEE.; 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998 ; Conference date: 21-06-1998 Through 24-06-1998",

year = "1998",

month = jan,

day = "1",

doi = "10.1109/LICS.1998.705651",

language = "English",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "141--152",

booktitle = "Proceedings - 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998",

}

Fages, F, Ruet, P & Soliman, S 1998, Phase semantics and verification of concurrent constraint programs. in Proceedings - 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998. Proceedings - Symposium on Logic in Computer Science, vol. 1998-June, Institute of Electrical and Electronics Engineers Inc., pp. 141-152, 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998, Indianapolis, United States, 21/06/98. https://doi.org/10.1109/LICS.1998.705651

Phase semantics and verification of concurrent constraint programs. / Fages, François; Ruet, Paul; Soliman, Sylvain.
Proceedings - 13th Annual IEEE Symposium on Logic in Computer Science, LICS 1998. Institute of Electrical and Electronics Engineers Inc., 1998. p. 141-152 (Proceedings - Symposium on Logic in Computer Science; Vol. 1998-June).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Phase semantics and verification of concurrent constraint programs

AU - Fages, François

AU - Ruet, Paul

AU - Soliman, Sylvain

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 -

Phase semantics and verification of concurrent constraint programs

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this