What is a Constraint System?

Prakash Panangaden^{∗}, McGill University Vijay Saraswat, Xerox PARC P. J. Scott^{†}, University of Ottawa

R. A. G. Seely^{‡}, McGill University and John Abbott College

December 8, 1991

Abstract

We study a relationship between logic and computation via concurrent constraint programming. In previous papers it has been shown how a simple language for asynchronous concurrent processes can be interpreted in terms of constraints. In the present paper we show that the programming interpretation via closure operators is intimately related to the logic of the constraints. More precisely we show how the usual hyperdoctrinal description of first order logic can be functorially related to another hyperdoctrine built out of closure operators. The logical connectives map onto constructions on closure operators that turn out to model programming constructs, specifically conjunction becomes parallel composition and existential quantification becomes hiding of local variables.

∗Research supported by an operating grant from the Natural Sciences and Engineering Research Council and a team grant from Fonds pour la Formation de Chercheurs et l’Aide á la Recherche (Québec).

†Research supported by an operating grant from the Natural Sciences and Engineering Research Council, a team grant from Fonds pour la Formation de Chercheurs et l’Aide á la Recherche (Québec), and the Ontario Ministry of Colleges and Universities Ontario-Québec Exchange.

‡Research supported by Fonds pour la Formation de Chercheurs et l’Aide á la Recherche (Québec) and an operating grant from the Natural Sciences and Engineering Research Council

1 Introduction

This paper develops a category theoretic view of the relationship between concurrent constraint programming (CCP) and logic. One may think of this as an explication of the relationship between logic and what is often called logic programming. The present treatment takes some new directions from the usual study that links the operational semantics to the model theoretic semantics (e.g. [1]) because of the desire to handle concurrency and synchronization in a logical way. Briefly these directions are: (i) the mathematical semantics is based on the idea of programs as information transducers; in the spirit of denotational semantics, programs are modelled as closure operators on certain algebraic lattices and (ii) the semantics treats concurrency in a natural and simple way; parallel composition of processes is one of the easiest combinators to describe.

The CCP paradigm can be described in the following way. The crucial concept underlying this paradigm is to replace the notion of store-as-valuation behind imperative programming languages with the notion of store-as-constraint. A constraint is just a partial specification of the values of variables (e.g., X ≥ Y +Z). Thus the usual notion of a “store” is replaced by the notion of a variable that may only be partly defined. This shift to partially specified values renders the usual notions of (imperative) “write” and “read” incoherent.

Instead, [15] proposes the replacement of read with the notion of Ask and write with the notion of Tell. An Ask operation takes a constraint (say, c) and uses it to probe the structure of the store. It succeeds if the store contains enough information to entail c. Tell takes a constraint and conjoins it to the constraints already in place in the store. That is, the set of valuations describing the resultant store is the intersection of the set of valuations describing the original store and those describing the additional constraint. Thus, as computation progresses, more and more information is accumulated in the store—a basic step does not change the value of a variable but rules out certain values that were possible before; the store is monotonically refined.

This simple view of computation can be seen as arising as a purification of logic programming [15], an enhancement of functional programming, a generalization of imperative programming, and a bidirectional generalization of dataflow programming (cf., the I-structures of Id Nouveau [9]). From the viewpoint of programming languages, the important contribution of the CCP paradigm is that the programmer can work directly with the notion of partial information. In other words, programming constructs provide direct access to the underlying information order. For this reason the present semantics, described and shown fully abstract in [13], is important.

This paper has two main contributions. First, we propose to view constraint systems as certain hyperdoctrines, obtained from the usual categorical account of first-order logic by restricting our attention to the logic of conjunction and existential quantification. Second, we construct a hyperdoctrinal structure of closure operators and show that it arises as a functorial image of the first, with the (functorial images of) conjunction and existential quantification exactly matching the constructions on closure operators used to model parallel composition and hiding (local variables). Thus the functor describes the passage from logical constructs to program combinators in a simple and pleasing way.

The idea of monotonic update is central to the theoretical treatment of Istructures in Id Nouveau [9]. From the viewpoint of dataflow programming, the concurrent constraint paradigm is also a generalization in that the flow of information between two processes is bidirectional.

The one other categorical approach to logic programming that we are aware of, by Asperti [2] has a different focus. Like us he uses categorical machinery to avoid talking about variables. However, he is interested in modelling the SLD resolution process whereas our intention is to study a semntical theory of concurrent constraint program based on closure operators.

The rest of this paper is as follows. The next section briefly summarizes the theory of concurrent constraint languages [12, 13]. (A detailed discussion of programming idioms within this paradigm is contained in the forthcoming book by Saraswat [15].) Subsequently, we describe the hyperdoctrine of constraintsystems. Finally, we describe the hyperdoctrine of closure operators and exhibit its functorial connection with constraint systems. We conclude with a brief discussion of the possibilities for future work opened up by this paper.

Semantics of Concurrent Constraint Languages

The discussion in this subsection is a condensation of the discussion in [13]. The syntax and operational semantics of the language are given in Table 1. We use the letter c to stand for an element of the constraint system. The basic combinators are the ask and tell written c → A and c respectively. Intuitively, c → A executes by asking the store whether c holds, if it does than A executes otherwise the process suspends. The tell combinator c simply asserts the constraint c. The parallel composition of two agents is written A_{1}||A_{2}. Hiding is written new x in A. Finally we have procedure calls, including possibly recursive procedures but we exclude them from the present discussion. The syntax and operational semantics of the language are given in Table 1.

In the description of the operational semantics one can already see that there is a relation with a sequent style presentation of logic. In the rule for new x in A, we have assumed that x is not free in Γ or in s.

In the denotational semantics one models processes as closure operators. Speaking operationally, in order to model a process compositionally, it suffices to record its resting points. Mathematically, this is mirrored by the fact that a closure operator is completely specified by its set of fixed points. One can define intersection of sets of fixed points of closure operators. It turns out that this operation is exactly what one needs to model parallel composition. The denotational semantics is given in 2. We have left out details like the Syntax.

A::=c | c → A | A||A | new x in A

Configurations are pairs, consisting of a (possibly empty) multiset of agents, written Γ and a (possibly empty) multiset of primitive constraints, the store, written s. The transition relation is defined between configurations.

⟨(Γ, A_{1} ∥ A_{2}), s⟩  ⟶ ⟨(Γ, A_{1}, A_{2}), s⟩
⟨(Γ, new x in A), s⟩ ⟶ ⟨(Γ, A), s⟩
⟨(Γ, c ⟶ A), s⟩  ⟶ ⟨(Γ, A), s⟩ where s ⊢ c
⟨(Γ, c), s⟩  ⟶ ⟨Γ, (s, c)⟩

Table 1: Operational semantics for the Ask-and-Tell cc languages

Syntax.

A::=c | c → A | A ∥ A | new X in A

Semantic Equations.

A c = {d ∈ |D| | d ≥ c}
A c → A = {d ∈ |D| | d ≥ c⇒d ∈ A A }
A A ∥ B = {d ∈ |D| | d ∈ A A ∧ d ∈ A B }
A new X in A = {d ∈ |D| | ∃c ∈ A A .∃_{X}d = ∃_{X}c}

Above, c ranges over basic constraints, that is, finite sets of tokens.

Table 2: Denotational Semantics for the Ask-and-Tell cc languages

definition of the environment mechanism and procedures. The closure operators are described by giving their set of fixed points.

2 Constraint Systems as Hyperdoctrines

In this section we review the connection, elucidated by Lawvere originally[11], between ordinary first-order logic and category theory through the use of hyperdoctrines. We will give a minimal and simplified account that only encompasses conjunction and existential quantification. These are the two connectives that any constraint system must have. There is nothing original in this section; we follow the ideas in Seely’s discussion [18] of the connection between theories in first order logic presented in a natural deduction format and hyperdoctrines. The most important point of this section is that in the hyperdoctrinal presentation is that one has a general abstract definition of existential quantification, which encompasses the usual logical notion, but which also carries over to other hyperdoctrinal structures, as we shall see in the next section.

In the hyperdoctrinal presentation, one has a family of categories, called the fibres, indexed by the objects of a cartesian category called the base category. Corresponding to the arrows of the base category are functors between the fibres. Thus, in general, a hyperdoctrine over the base category is a contravariant functor^{1} to CAT. For our purposes it will be sufficient to consider the fibres to be preordered sets.

We define a constriant system as a simplified hyperdoctrine.

Definition 2.1 A (hyperdoctrinal) constraint system is a contravariant functor P() : B^{op} ⟶ ∧ − Preord, where ∧ − Preord is the category of meetpreorders, and B is cartesian. We assume that for each arrow f in B, the (monotone) function P(f) (often written f^{∗}) preserves meets and has a left adjoint, written ∃_{f}. We also require the following two conditions:

1. Beck condition If the following diagram is a pullback

[figure: A′; B′; k; A; B; f; g; h]

and ϕ ∈ P(B) then ∃_{g}(f^{∗}ϕ) ∼ k^{∗}(∃_{h}ϕ), where ∼ means that we have two way entailment.

2. Frobenius Reciprocity: For each f : A ⟶ B in B and ϕ ∈ P(A) and ψ ∈ P(B) we have ∃_{f}(f^{∗}ψ ∧ ϕ) ⟶ ψ ∧ ∃_{f}ϕ.

In the case where we have a constraint system syntactically presented as a concrete theory in first order conjunctive logic with existential quantification the hyperdoctrine conditions are easy to check [18]. At the least, the base category is generated by a set of basic data values V : the objects of B are all finite products of V, including the empty product 1, and the arrows are the smallest set of arrows containing all the projections and identity arrows, and closed under composition and pairing. In general there may be other arrows between objects corresponding to terms.

Convention 2.1 Since the objects of B are indexed by nonnegative integers we will usually just write n when we mean the object V^{n} of B.

Convention 2.2 We will use greek letters like ϕ, ψ etc. to stand for formulas.

1Generally these are pseudofunctors but in the posetal situation that we consider it does not make any difference.

Definition 2.2 Given a concrete constraint system we define a functor P() from B^{op} to ∧ − Preord as follows. The functor P() takes an object n to the formulas with n free variables constructed out of terms, variables, predicate symbols, conjunction and existential quantification. The preorder describes the entailment relation. Thus, if ϕ ⊢ ψ we define ϕ ≤ ψ, or, equivalently, ϕ → ψ. If f is an arrow from m to n in B, we define P(f) from P(n) to P(m) by P(f)(ϕ)[X⃗] = (ϕ)[f(Y⃗)], where X⃗ and Y⃗ are vectors of variables.

Note that the arrows P(f) are clearly meet preserving when f is one of the projection maps, because all this means in this case is that adjoining dummy variables is defined structurally.

Now we give the abstract definition of existential quantification as the left adjoint to substitution. Consider, for definiteness, the fibres over 1 and 2, i.e. P(1) and P(2). Recall that 2 is just 1×1, let p be the first projection from 2 to 1. The functor (monotone function between preorders), P(p), written p^{∗}, from P(1) to P(2) is, according to the above, just p^{∗}(ϕ)[X] = ϕ[p(X, Y)]. Because p^{∗} preserves meets, it has a left adjoint^{2}, written ∃_{p}, a functor from P(2) to P(1). In fact,

∃_{p}.ψ[X, Y] = ∃X′∃Y′(p(X′, Y′) = X ∧ ψ[X′, Y′]).

By Tarski’s trick, this equals ∃Y′ψ[X, Y′] . It is easy to prove directly (for intuitionistic first order logic with equality) that ∃_{p} is left adjoint to subsitution p^{∗}. All this clearly extends to other maps between other fibres and to the multisorted case.

Defined this way, the functor enjoys all the properties one normally expects of existential quantification. For example ϕ ≤ p^{∗}(∃_{p}ϕ) is immediate and means the same as what is traditionally written as ϕ ≤ ∃_{X}.ϕ.

The Beck condition that we discussed above needs to be checked for only a few simple classes of diagrams. When the constraint system is derived from syntax these are easily checkable formulas. Frobenius reciprocity, when one has implication, is equivalent to saying that the maps of the form f^{∗} preserve implication. In the absence of an implication in the fibres we demand Frobenius reciprocity as a condition. Again in the concrete case one can checj Frobenius easily. Seely [18] shows how one can go back and forth between the hyperdoctrinal presentation of a first order theory in and the more traditional presentation of such theories in a natural deduction format.

3 A Hyperdoctrine of Closure Operators

In this section we show how one can build two new hyperdoctrines, by defining a suitable functor from meet-Preord to CAL, the category of complete algebraic lattices and then an endofunctor on CAL. Roughly speaking the first functor takes us from logic to “information structure” in a familiar way and the second takes us from an information structure to a collection of closure operators. The main point of this construction is that it provides the promised tie up between existential quantification in the logic and block structure at the program level. The main technical difficulty is actually finding the functor that produces the last hyperdoctrine. We give proofs at the lemma and theorem level. The detailed proofs of lemmas that we have omitted are easy.

2This is easily proved for Galois connections between posets, see for example [4].

The category meet-Preord has preordered sets equipped with binary meets as objects and monotone functions as the morphisms. The category we actually use is not quite CAL but instead CAL^{adj} which has complete algebraic lattices as objects and adjunction pairs as morphisms.

Definition 3.1 The objects of the category CAL^{adj} are complete algebraic lattices. A morphism m from L to M is a adjunction pair between L and M. In more detail, a morphism m from L to M is a pair of monotone functions, ⟨f : L → M, g : M → L⟩ with f left adjoint to g (i.e. f ⊣ g). The composition of morphisms ⟨f, g⟩ and ⟨h, k⟩ is ⟨h ∘ f, g ∘ k⟩.

By the adjoint functor theorem, f preserves arbitrary sups.

The lattices in question are obtained by taking entailment closed sets of formulas or “theories”. Since this hyperdoctrine arises by composing the previous hyperdoctrine with a functor, the Beck conditions and Frobenius reciprocity hold automatically.

We can define a functor, F(), from meet-Preord to CAL as follows. In the next few paragraphs let A and B be meet preorders and m : A → B a monotone function between them.

Definition 3.2 A filter in A is an upwards closed set that is also closed under the formation of binary (and hence all finitary) meets.

Definition 3.3 The lattice F(A) is defined to be the set of filters of A ordered by inclusion.

Convention 3.1 We use letters like u, v, w to stand for elements of the complete algebraic lattices generated in this way.

Notation 3.1 Given ϕ an element of A, we write (ϕ) ↑ for the principal filter generated by ϕ. For any subset A′ of A we write (A′) ↑ for ⋃_{ϕ∈A}(ϕ) ↑.

Note that with our choice of ordering we have ϕ ≤ ψ ⇒ (ψ) ↑ ⊑ (ϕ) ↑.

Notation 3.2 Given any set X, a function f from X to X′ and a subset Y of X we write f(Y′) for the direct image {f(y)|y ∈ Y }.

Definition 3.4 The arrow part of the functor F(), is given by mapping the monotone function m to the pair, ⟨F(m), m^{−1}⟩, where F(m) from F(A) to F(B) is given by u ↦ (m(u)) ↑ where u ∈ F(A) and m^{−1} is inverse image.

Proposition 3.5 If A is a meet-preorder then F(A) is a complete algebraic lattice with joins given by upward closures of unions and meets given by intersections. If m is a monotone function from A to B then ⟨F(m), m^{−1}⟩ is an adjunction pair from F(A) to F(B). F() defined in this way is a functor.

In fact we can think of F() as going from adjunction pairs to adjunction pairs. In view of this we have the following theorem.

Theorem 3.6 The composition of the functors F() and P() produces another hyperdoctrinal constraint system on B with (p^{∗})^{−1} right adjoint to F(p^{∗}).

A simple calculation shows that (p^{∗})^{−1} is in fact F(∃_{p}). We will often write ⟨F(p^{∗}), F(∃_{p})⟩ rather than ⟨F(p^{∗}), (p^{∗})^{−1}⟩, to emphasize the role of existential quantification.

We consider closure operators over the lattices produced in the last hyperdoctrine. The formal definition of closure operators and some basic facts about them [16, 4] appear in the appendix.

Notation 3.3 We write Cl(L) for the set of closure operators on a lattice L.

Now we define a hyperdoctrine of lattices by taking the closure operators on the lattces that form the fibres in the previous hyperdoctrine. Once again we will define the new hyperdoctrine as the functorial image of the preceding hyperdoctrine.

We recall the following technique, due to Dana Scott, for lifting adjunctions between posets to adjunctions between their endofunction spaces.

Proposition 3.7 Suppose that ⟨f, g⟩ is a morphism^{3} in CAL^{adj} from L to M. Then ⟨f′, g′⟩ is a morphism from [L → L] to [M → M]; where f′ = λh : [L → L].f ∘ h ∘ g g′ = λk : [M → M].g ∘ k ∘ f

The basic idea is to try to define an endofunctor from CAL^{adj} to CAL^{adj} as follows. We map an object L (a complete algebraic lattice) to the set of all closure operators on L ordered pointwise. For the arrow part of the functor, we define it by saying that it maps a morphism ⟨f, g⟩ from L to M to ⟨f′, g′⟩ as defined in the last proposition. Since the closure operators on L are a sublattice of [L → L] we should have another adjoint pair and hence a morphism of CAL^{adj}. Unfortunately, however, given h, a closure operator on L, f ∘ h ∘ g need not be a closure operator on L.

In order to get around the above difficulty we use a remarkable function, V, discussed by Scott [16]. The function V maps functions on [D → D] to closure operators on D. It turns out that V is itself a closure operator on [[D → D] → [D → D]] whose fixed points are exactly the closure operators. In our discussion we use the characterization of closure operators in terms of their sets of fixed points.

3We only use the fact that they form an adjunction.

Lemma 3.8 If f is any monotone function in [D → D], where D is any poset, then {x ∈ D|f(x) ≤ x} is closed under the formation of meets insofar as they exist.

Definition 3.9 Suppose that f is a function in [D → D] where D is any poset. We define the function V in [[D → D] → [D → D]] by V (f) = clo({x ∈ D|f(x) ≤ x}).

The lemma tells us that the definition just above makes sense. Thus, using V, we may take any monotone endofunction and convert it into a closure operator by applying V to it.

Notation 3.4 Suppose that f is a monotone function in [D → D] we write \overline{f} for V (f).

Comment 3.1 Note that \overline{f} is the least closure operator extensionally greater than f.

Lemma 3.10 If ⟨f, g⟩ is a morphism in CAL^{adj} from L to M then ⟨f′, g′⟩ is a morphism in CAL^{adj} from Cl(L) to Cl(M) where f′ = λh : Cl(L).\overline{f ∘ h ∘ g} and g′ = λk : Cl(M).\overline{g ∘ k ∘ f}.

We can now define the promised endofunctor on CAL^{adj}.

Definition 3.11 The functor Cl(−) from CAL^{adj} to CAL^{adj} is defined as follows. It takes a complete algebraic lattice L to the complete algebraic lattice of closure operators on L ordered extensionally (reverse inclusion of the sets of fixed points). It takes a morphism ⟨f, g⟩ from L to M to the morphism ⟨f′, g′⟩ where f′ = λh : [L → L].\overline{f ∘ h ∘ g} g′ = λk : [M → M].\overline{g ∘ k ∘ f}.

In order to prove this, however, it is much easier to describe the arrow part of the functor in terms of the effects on sets of fixed points.

Lemma 3.12 Suppose that ⟨f, g⟩ is a morhism from L to M with h ∈ Cl(L) and k ∈ Cl(M). Then \overline{g ∘ k ∘ f} = g(fix(k)) and \overline{f ∘ h ∘ g} = g^{−1}(fix(h)).

With this in hand the proof of the folowing is easy.

Lemma 3.13 Cl(⟨f_{1}, g_{1}⟩) ∘ Cl(⟨f_{2}, g_{2}⟩) = Cl(⟨f_{1} ∘ f_{2}, g_{1} ∘ g_{2}⟩).

These lemmas have allowed us to claim the following theorem:

Theorem 3.14 The composition of the functors Cl(−) ∘ F(−) ∘ P(−) produces a hyperdoctrinal constraint system.

Since we have defined it as acting on adjoint pairs it is evident that the hyperdoctrinal structure on CAL^{adj} is carried over to the closure operators.

One can now inspect the table for the denotational semantics of the concurrent constraint language and see that the definintion of the construct new X in A uses the concrete version of the existential quantification operation in the last hyperdoctrine. Parallel composition is modelled by the sup operation in the lattices which is, of course comes ultimately from the meet operation in the first hyperdoctrine.

4 Conclusions

We view the results of this paper as the start of a larger investigation in the same spirit. The most important direction is to formulate a notion of higher order constraint programming. Higher order process calculi are starting to be studied in earnest especially those related to the lambda calculus [3, 8]. Recently, Jagadeesan and Pingali [7] have presented a higher-order version of Id, a functional language with logical variables, and Saraswat [14] has developed the notion of higher-order concurrent constraint programming. We expect to study properties of the category of constraint systems of [14], by extending the techniques of this paper. For example, we expect to obtain this category by applying some standard constructions, such as Grothendeick fibration, to the hyperdoctrinal structures of Section 3.

The other important direction to pursue is the study of other logical combinators and process combinators. In particular, we expect to explore the categorical implications of adding disjunction, negation, implication and universal quantification to the computational setting.

A Closure operators

In order to avoid confusion in comparing our statements with those in the compendium we note that we say “left adjoint” where the compendium would say “lower adjoint” and similarly we say “right adjoint” where the compendium would say “upper adjoint”.

Definition A.1 Given a lattice L a function c from L to L is a closure operator if c is monotone, idempotent, i.e. c = c ∘ c, and increasing (extensive), i.e. ∀x ∈ L.x ≤ c(x).

The following proposition, taken from pages 21 and 22 of [4], gives an equivalent characterization of closure operators.

Proposition A.2 Let f be a monotone function from L to L. Let f^{∘} be the corestriction to the image f^{∘} : L → f(L) and let f_{∘} be the inclusion of the image of f in L, f_{∘} : f(L) → L. Then f is a closure operator iff f^{∘} is right adjoint to f_{∘}.

The next two propositions relate a closure operator with its set of fixed points.

Proposition A.3 The set of fixed points of a closure operator are closed under the formation of meets (infs) to the extent that they exist.

Proposition A.4 Let L be a complete lattice. Let Cl(L) be the set of closure operators on L ordered extensionally. Let C(L) be the set of meet-closed subsets of L ordered by reverse inclusion. Then the map fix : Cl(L) → C(L) that takes a closure operator to its image (which is its set of fixed points) is an order isomorphism. The inverse of fix is the map clo : C(L) → Cl(L) given by clo(S)(x) = min((x) ↑ ∩ S) = inf((x) ↑ ∩ S).

Proposition A.5 The collection of closure operators on a complete algebraic lattice ordered extensionally, form a complete algebraic lattice.

References

[1] K.R Apt and M.H. van Emden. Contributions to the theory of logic programming. JACM, 29(3):841–862, 1982.

[2] A. G. Asperti. Categorical Topics in Computer Science. Doctoral dissertation, dipartmento di informatica, University of Pisa.

[3] G. Boudol. Towards a lambda-calculus for concurrent and communicating systems. In J. Diaz, editor, TAPSOFT 89, Lecture Notes in Computer Science 351, pages 149–161. Springer-Verlag, 1989.

[4] G.Gierz, K.H.Hoffman, K.Keimel, J.D.Lawson, M.Mislove, and D.S.Scott, editors. A compendium of continuous lattices. Springer-Verlag Berlin Heidelberg New York, 1980.

[5] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.

[6] Leon Henkin, J. Donald Monk, and Alfred Tarski. Cylindric Algebras (Part I). North Holland Publishing Company, 1971.

[7] R. Jagadeesan, and K. Pingali. Abstract Semantics for a higher-order functional language with logic variables. In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, 1992.

[8] R. Jagadeesan and P. Panangaden. A domain-theoretic model of a higherorder process calculus. In M. Paterson, editor, Proceedings of the 17th International Colloquium on Automata Languages and Programming, pages 181–194. Springer-Verlag, 1990. Lecture Notes in Computer Science 443.

[9] R. Jagadeesan, P. Panangaden, and K. Pingali. A fully abstract semantics for a functional language with logic variables. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 294–303, 1989.

[10] R.A. Kowalski and M.H. van Emden. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733–742, 1976.

[11] F. W. Lawvere. Functorial semantics of algebraic theories. Proc. Nat. Acad. Sci. U.S.A., 50:869–872, 1963.

[12] Vijay Saraswat and Martin Rinard. Concurrent constraint programming. In Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 232–245, 1990.

[13] Vijay Saraswat, Martin Rinard, and Prakash Panangaden. Semantic foundations of concurrent constraint programming. In Proceedings of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991.

[14] Vijay Saraswat. Concurrency in the λ-calculus: higher order concurrent constraint programming Unpublished.

[15] Vijay A. Saraswat. Concurrent Constraint Programming Languages. PhD thesis, Carnegie-Mellon University, January 1989. To appear, Doctoral Dissertation Award and Logic Programming Series, MIT Press, 1990.

[16] D. Scott. Data types as lattices. SIAM Journal of Computing, 5(3):522– 587, 1976.

[17] D. S. Scott. Domains for denotational semantics. In Ninth International Colloquium On Automata Languages And Programming. Springer-Verlag, 1982. Lecture Notes In Computer Science 140.

[18] R. A. G. Seely. Hyperdoctrines, natural deduction and the beck conditions. Zeitschr. f. math. Logik und Grundlagen d. Math., vol 29, pp 505–542, 1983.