Linear concurrent constraint programming: Operational and phase semantics

In this paper we give a logical semantics for the class CC of concurrent co nstraint programming languages and for its extension LCC based on linear co nstraint systems. Besides the characterization in intuitionistic logic of t he stores of CC computations, we show that both the stoles and the successe s of LCC computations can be characterized in intuitionistic linear logic. We illustrate the usefulness of these results by showing with examples how the phase semantics of linear logic can be used to give simple "semantical" proofs of safety properties of LCC programs. (C) 2001 Academic Press.