Paper: Phase Semantics and Verification of Concurrent Constraint Programs (at LICS 1998)

Authors: François Fages Paul Ruet Sylvain Soliman

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

BibTeX

  @InProceedings{FagesRuetSoliman-PhaseSemanticsandVe,
    author = 	 {François Fages and Paul Ruet and Sylvain Soliman},
    title = 	 {Phase Semantics and Verification of Concurrent Constraint Programs},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {141--152},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }