Concurrent Constraint Programming and Linear Logic

Series: Logic Seminar

Date: Tuesday, October 19, 1999

Speaker: Francois Fages (DMI, ENS, Paris)

Title: Concurrent Constraint Programming and Linear Logic

Time: 2:30 - 3:20 PM

Place: 122 Thomas Building

Abstract: 

The class CC(X) of concurrent constraint programming languages
introduced by Vijay Saraswat in the late 80's generalizes (constraint)
logic programs with the addition of an operator for expressing
concurrency and synchronization.  The well known logical properties of
constraint logic programs are no longer valid for CC because of the
possibility for a computation to suspend. Some observable properties
of CC programs can be captured however by translating CC programs into
formulas of Intuitionistic Logic. We show that a translation of CC
programs into formulas of Jean Yves Girard's Linear Logic provides a
more refined logical semantics that allows us to characterize both the
set of accessible stores and the set of success stores of CC
computations. We show how these results can be used to verify CC
programs. We present also some limits of this approach that led to the
definition of the Non-Commutative Logic of Paul Ruet.