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.
Note: A related paper Proofs as Concurrent Processes is available.