• 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