Concurrent constraint programs operate on data which is represented by a constraint of a given cylindric constraint system. Such a system provides an algebraic representation of first-order logic. It features a (binary) entailment relation, a binary union operation for adding information (formally defined as the least upper bound of two constraints with respect to the entailment relation) and, and finally, existential quantification of variables.

In this lecture we discuss a sound and complete proof theory based on traces of input/output constraints for reasoning about the correctness of concurrent constraint programs.