Series: Penn State Logic Seminar

Date: Tuesday, April 15, 2003

Time: 2:30 - 3:45 PM

Place: 113A Chambers Building

Speaker: Vijay Saraswat, Penn State, Computer Science and Engineering

Title: The Logic of Concurrent Constraint Programming

Abstract: 

Over the last fifteen years, I have been developing the theory of
concurrent constraint programming (CCP) with various colleagues. CCP
may perhaps be considered the richest theory of *determinate*
concurrency: execution of a program is guaranteed to yield a single
answer. The framework is based on the simple idea of agents
communicating by exchanging pieces of partial information
(constraints) on shared variables. Communication is accumulative,
leading to a simple characterization of programs as closure operators
over an underlying (cylindric) algebra of constraints. The theory has
been extended with a notion of discrete time, following the Synchrony
hypothesis of Berry and others, yielding the discrete timed CCP
languages, and with a notion of defaults in order to permit the
expression of instantaneous pre-emption.  It has also been extended to
a notion of continuous time, yielding the notion of *hybrid programs*,
whose execution is characterizing by the tracing out of mostly smooth
trajectories.

In this talk I will survey the underlying logical foundations for
CCP. The core determinate calculus is easily seen as performing
deductions in a fragment of intuitionistic logic. We present a
completeness theorem for CCP deductions utilizing a notion of normal
proofs (joint work with P Lincoln). We show how this interpretation
can be extended to the default discrete timed case (joint work with R
Jagadeesan and V Gupta).  We will touch on extensions of this basic
computational interpretation to linear logic, and on connections with
Dale Miller et al's FOLD logic.  Time permitting we will also discuss
some recent work on a higher-order version of CCP which relies on a
novel (to our knowledge) symmetric interpretation of application in
the lambda calculus. Various open problems will be discussed.