Two Models of Synthetic Domain Theory

Dedicated to Peter Freyd on the occasion of his 60^{th} birthday

Marcelo P. Fiore^{a,1}, Giuseppe Rosolini^{b,2}

a LFCS, The King’s Buildings, Edinburgh EH9 3JZ, Scotland b DIMA, via Dodecaneso 35, 16146 Genova, Italy

Two models of synthetic domain theory encompassing traditional categories of domains are introduced. First, we present a Grothendieck topos embedding the category ω-Cpo of ω-complete posets and ω-continuous functions as a reflective exponential ideal. Second, we obtain analogous results with respect to a category of domains and stable functions.

Introduction

The first steps on Synthetic Domain Theory (SDT) were taken by Martin Hyland, see [8], after some work on Scott domains in realizability toposes in [13,12]. The idea at the core of the study was proposed by Dana Scott long before: domains should be certain “sets” in a mathematical universe where all functions between them would be continuous. The aim of SDT is to axiomatize the structure needed on a set-theoretic universe (e.g. a topos) so that the domains in it (e.g. the replete objects [8,17]) enjoy the properties needed in denotational semantics, e.g. closure under sums, products, and exponentials, the admission of fixed-point operators, and the solution of recursive domain equations. Further impulse to the abstract theory derived from the characterization of the categorical properties of the solutions of domain equations due to Peter Freyd [5,3,4]. In particular, after his insight of considering canonical maps from initial algebras to final coalgebras, the main infinitary axiom of SDT, see [8], reads as follows: (L1)^{c} is an iso, where 1 is a terminal object, L is (the underlying endofunctor of) a lifting monad [8,2] internalizing partial

1 Research supported by EC project Programming Language Semantics and Program Logics grant SC1000 795. 2 Research supported by EC project no.6811, CLICS II, and from MURST 40%.

Elsevier Preprint

computations, and c is the canonical map from the initial L-algebra to the final L-coalgebra.

This paper is concerned with models of SDT encompassing traditional categories of domains used in denotational semantics [7,18], showing that the synthetic approach generalises the standard theory of domains and suggests new problems to it.

Consider a (locally small) category of domains D with a (small) dense generator G equipped with a Grothendieck topology. Assume further that every cover in G is effective epimorphic in D. Then, by Yoneda, D embeds fully and faithfully in the topos of sheaves on G for the canonical topology, which thus provides a set-theoretic universe for our original category of domains. In this paper we explore such a situation for two traditional categories of domains and, in particular, show that the Grothendieck toposes so arising yield models of SDT. In a subsequent paper we will investigate intrinsic characterizations, within our models, of these categories of domains.

First, we present a model of SDT embedding the category ω-Cpo of posets with least upper bounds of countable chains (hence called ω-complete) and ω-continuous functions (i.e. monotone functions which preserve these lubs) as a reflective exponential ideal. In turn, ω-Cpo embeds the category of domains in the model, viz. the full subcategory of replete objects, again as a reflective exponential ideal. The replete ω-complete partial orders may offer a new interesting notion of domain to the standard theory but, at the moment, no explicit description of them is known.

Second, we give another model for a stable variant of SDT, produced by a simple change in the defining site, and obtain analogous results with respect to a category of domains and stable functions.

1 The topos of continuous \overline{ω}-paths

The first model is a topos obtained from the graph model of the λ-calculus [15]. The construction is similar to Mulry’s recursive topos; see [11] and, for a general treatment, [13].

We begin by fixing notation and by recalling a few facts. We denote the finite cardinals as 0 = ∅, …, n+1 = {0, …, n}, … and write N for the collection {0, …, n, …} of finite cardinals. We write n for the ordinal (n, ⊆) and for a chain x_{0} ≤ … ≤ x_{n−1} in a poset P we write (x_{0}, …, x_{n−1}) for the monotone map n ^{}P sending i to x_{i}. We further write ω for the ordinal (N, ⊆).

Write S(C) for the idempotent splitting of a category C, see [16,6]. Consider the poset (P(N), ⊆) of subsets of N ordered by inclusion, and the monoid P of ω-continuous endofunctions on it. Then S(P) fully embeds into the category ω-Cpo of ω-complete posets and ω-continuous functions as the full subcategory of continuous lattices [15].

The following is well known:

Lemma 1 S(P)^{⊂} ^{}_{full}ω-Cpo is closed under countable products and exponentials.

PROOF. In ω-Cpo one has P(N) ≅ 2^{N}. Then,

P(N)^{N} ≅ (2^{N})^{N} ≅ 2^{N×N} ≅ 2^{N} ≅ P(N),

hence countable products of retracts of P(N) are again retracts of P(N). Also 2^{P(N)} \underline{◁}_{⊂} P(N) is a retract, see [15]. For instance, a map f ∈ 2^{P(N)} is completely determined by the upward closed family of finite subsets which f takes to 1. The retraction is thus obtained by composing

2^{P(N)} ≅ Up(P_{fin}(N)) \underline{◁}_{⊂} P(P_{fin}(N)) ≅ P(N).

As a consequence

P(N)^{P(N)} ≅ (2^{N})^{(2^{N})} ≅ (2^{(2^{N})})^{N} \underline{◁}_{⊂} (2^{N})^{N} ≅ 2^{N} ≅ P(N),

hence exponentials of retracts of P(N) are retracts of P(N) as well.

Let \overline{ω} be the retract of P(N) whose elements are 0, …, n, …, N ordered by inclusion; a retraction sends X ⊆ N to the smallest initial segment which contains it.

Consider the following full subcategories of S(P):

– the monoid L of endomaps on \overline{ω},

– the category F of finite products of \overline{ω}.

The splitting S(L) is equivalent to the full subcategory of ω-Cpo consisting of \overline{ω} and the non-empty finite ordinals.

Remark 2 In ω-Cpo, \overline{ω} is a dense generator: for every D in ω-Cpo, writing G_{D} for the full subcategory of ω-Cpo/D consisting of those objects of the form \overline{ω} ^{}D, the colimit of the domain functor G_{D} ^{}ω-Cpo is (D, ⟨f⟩_{f∈G_{D}}).

Thus, the “Yoneda” functor Y: ω-Cpo ^{}Set^{L^{op}}: D ^{}ω-Cpo(−, D) is full and faithful, and preserves limits and exponentials.

Let H be the topos sh(P, can) of sheaves on P for the canonical topology. It is useful to have various presentations of the topos.

Theorem 3 The inclusions

L^{⊂} F  P

[figure: S(L); ∩; ⊂; S(F); ∩; ⊂; S(P); ∩]

induce equivalences

sh(L, can) ^{_{}≃} sh(F, can)  H

[figure: sh(S(L), can); ≃; ≃; sh(S(F), can); ≃; ≃; sh(S(P), can).; ≃]

PROOF. The vertical equivalences are obvious. For the others, we apply the Comparison Lemma, see [9], using the following characterization.

Lemma 4 The collection of non-empty families R of monos in S(L) with common codomain D such that

(i) for every x, y ∈ D there exists f ∈ R such that {x, y} ⊆ im(f), and (ii) for every unbounded countable chain ⟨x_{k}⟩_{k} in D there exists f ∈ R such

that {x_{k} | k ∈ N} ∩ im(f) is infinite

is a basis for the canonical topology on S(L).

PROOF. In S(L) every map factors as a retraction followed by a section; so epimorphisms are retractions. Moreover, the inverse image of a mono intersecting the image of a map is created by the forgetful functor S(L) ^{}Set. Now, to see that the collection in the statement of the lemma is stable under pullback, let g: D′ ^{}D be a map in S(L) and let R′ be the pullback of a family R satisfying (i) and (ii). That R′ satisfies (i) is trivial. For (ii), there are two cases: im(g) is either finite or infinite. In the first case, there is a map in R′ whose image is closed upward, hence intersects every unbounded chain in an infinite set. Else, take an unbounded chain ⟨x_{k}⟩_{k} in D′ and consider ⟨g(x_{k})⟩_{k}: there is f ∈ R such that {g(x_{k}) | k ∈ N} ∩ im(f) is infinite. This set is the image under g of {x_{k} | k ∈ N} ∩ g^{−1}[im(f)], which is therefore infinite. It follows that the collection in the statement of the lemma is a basis for a topology, since clearly every isomorphism satisfies (i) and (ii), and the transitivity axiom holds. It is easy to prove that the topology is subcanonical, since D = ⋃_{f∈R} im(f) for any cover R of D in S(L). To prove that a stable effective epimorphic cover satisfies (i) and (ii); notice that if it does not satisfies (i) then the family {0: 1 ^{}2, 1: 1 ^{}2} does not cover 2 effectively; analogously, if it does not satisfies (ii) then one can construct a cover of \overline{ω} consisting only of finite subsets which cannot be effective (otherwise one could define a function \overline{ω} ^{}2 in S(L) sending all finite ordinals to 0 and N to 1).

To finish the proof of Theorem 3, observe that the description of Lemma 4 also applies to the canonical topology on the monoid L and the other categories. As for every D in S(P) the chains \overline{ω} ^{}D form a stable effective epimorphic family in S(P), every object in either of the categories F, S(F) and S(P) has a cover in the canonical topology whose domains are always \overline{ω}; moreover these covers generate the canonical topology.

When proving subcanonicity in Lemma 4, we essentially proved that: for an ω-complete poset D, the functor Y (D) is a sheaf, viz. the sheaf of continuous \overline{ω}-paths in D.

Theorem 5 The functor Y: ω-Cpo ^{}H presents ω-Cpo as a full reflective exponential ideal of H.

PROOF. By Remark 2, the functor Y is full and faithful, and preserves limits. From this, using that every sheaf is a colimit of representables, it is easy to see that ω-Cpo is an exponential ideal of H. By the Special Adjoint Functor Theorem, the functor Y has a left adjoint.

We characterize the closure under isomorphism of the image of Y; it is then convenient to see H as sh(S(F), can). A sheaf F in H is (isomorphic to) Y (D) for some D in ω-Cpo when it takes

1 [figure: 0; 1] 2  (R)

to a jointly monic pair, and takes the following colimits in S(F) to limits in Set

[figure: 1; 0; 2; 2; 1; (0, 1); 3; (1, 2)]  (T)

[figure: 1; 0; 2; 3; 1]  (A)

[figure: 2 × 1; id × 0; 2 × 2; id × (0, 1); 2 × 3; …; …; 2 × \overline{ω}.]  (C_{2})

Indeed, F (R) is a jointly monic pair if and only if ⟨F 0, F 1⟩: F (2) ^{}F (1) × F (1) is a binary relation on F (1). This is reflexive as F is a presheaf, and transitive because F (T) is a pullback. The fact that F (A) is an equalizer restates antisymmetry of the relation F (2) on F (1). Moreover, using sheaf conditions, one sees that the limit of

[figure: F 1; F 0; F 2; F (0, 1); F 3; …]

consists of the ω-chains in F (1). As F (C_{2}) is a limit diagram, the sheaf F also takes the following colimit in S(F)

[figure: 1; 0; 2; (0, 1); 3; …; …; \overline{ω}]  (C_{1})

to a limit in Set, and the map F (N): F (\overline{ω}) ^{}F (1) provides a candidate for the lub operation. It gives an upper bound because the diagrams

[figure: 1; 0; 2; 1; 1]
[figure: n; N; n ∈ N]
\overline{ω} (n, N)_{}

commute. Using more sheaf conditions, one checks that elements of F (2 × n) are pairs of chains of length n with the pointwise order. Then, from the fact that F (C_{2}) is a limit diagram, one shows that F (N) is monotone. Finally, it follows from the trivial commutativity of the diagram

[figure: 1; 0; 2; (0, 1); 3; …]

[figure] [figure] [figure: …]

1

that evaluating F (N) at a constant chain gives the constant value. This yields the required characterization.

Note that (R) being transformed in a jointly monic pair by F can be restated as a limit condition: the diagram

[figure: 1; 0; 1; 1; 2; 2; 1; 0; id; 2; id]  (R′)

is a colimit in S(L), and F takes it to a limit in Set if and only if F transforms (R) in a jointly monic pair.

Henceforth we shall identify an ω-complete poset D with the sheaf of its continuous \overline{ω}-paths Y (D).

2 H as a model of SDT

We show that H is a model of synthetic domain theory as in [8].

We write 1 for the terminal object Y (1), Σ for the sheaf of continuous \overline{ω}-paths Y (2) associated to the Sierpinski space 2, and ⊤: 1 ^{}Σ for Y (1: 1 ^{}2).

In H, the map ⊤: 1 ^{}Σ is a dominance, see [13]. It follows from loc.cit. that it induces a notion of composable partial map in H, with a representation. We shall denote by L the action of the representation functor on H which underlies the so-called lifting monad.

The above abstract construction extends a well-known behaviour on the category ω-Cpo. Indeed, the notion of partial map is that expected from partial computations, see [2]. In ω-Cpo one can consider partial maps defined on a Scott-open subset. A Scott-open subset is a monomorphism in ω-Cpo which reflects the order and whose image is upward closed and inaccessible by sups of ω-chains. The representing functor adds an element below the given order.

The lifting monad migrates to other subcategories of H.

Proposition 6 The functor L: H ^{}H restricts to the endofunctor on the subcategory ω-Cpo which represents partial maps defined on Scott-open subsets. Moreover, the functor L restricts to the sites defining H. In other words there are functors such that the diagram

[figure: S(L); ⊂; S(F); ⊂; S(P); ⊂; ω-Cpo; ⊂; Y; H]

[figure: S(L); L; ⊂; S(F); ⊂; S(P); ⊂; ω-Cpo; ⊂; Y; H; L]

commutes up to isomorphism. As the inclusions are full, all restrictions induce monads.

Note that S(L), S(F), and S(P) cannot sustain a notion of partial map on Scott-open subsets as they miss an initial object. For later reference, also note that L on S(L) is

L: S(L) \overline{}S(L)
n n + 1
\overline{ω}  \overline{ω}

with unit given by the successor function.

Another functor representing a different kind of partial map can be defined on H: consider the notion of Scott-closed subset as just the complement of a Scott-open subset. Explicitly, a monomorphism in ω-Cpo is Scott-closed if it reflects the order and its image is closed downward and under sups of ω-chains. The representing functor adds an element above the given order. The notion of partiality is that induced by the dominance ⊥: 1 ^{}Σ, defined as Y (0: 1 ^{}2), in H.

It is convenient to notice some other properties of L on the sites.

Lemma 7 (i) The functor Σ^{(−)}: S(P) ^{}S(P) applies S(L) into itself. (ii) The map ς: \overline{ω} ^{}L\overline{ω}: x ^{}x is a final L-coalgebra in S(L).

PROOF. (i) Σ\overline{ω} ≅ Open(\overline{ω}) ≅ L\overline{ω} ≅ \overline{ω}. (ii) The diagram

[figure: 1; i; L1 = 2; Li; L^{2}1 = 3; L^{2}i; …]
[figure: …]
\overline{ω}

is a limit in S(L) and it is easy to see that L transforms it in a diagram with the same limit vertex.

So to see H as a model of the axioms of synthetic domain theory as in [8] we take the disjoint dominances ⊤: 1 ^{}Σ and ⊥: 1 ^{}Σ.

The map Σ^{[⊥,⊤]}: Σ^{Σ} ^{}Σ^{1+1} is monic by Theorem 5 and Lemma 7(i) because (A) is jointly monic in S(L). The object Σ is a sup-lattice with countable joins Σ^{N} ^{}Σ in H, because it is such in S(P).

Finally, consider the initial L-algebra and the final L-coalgebra in H: these are fairly simple to compute. For the final coalgebra note that \overline{ω} is a final L-coalgebra in S(L) obtained as the limit of the diagram

[figure: 1; i; L1; Li; L^{2}1; L^{2}i; …]

As the Yoneda embedding preserves limits, and commutes with L, the object \overline{ω} remains a final L-coalgebra in H.

Since we already know an L-algebra ς^{−1}: L(\overline{ω}) ^{}\overline{ω} whose structure is an isomorphism, the initial algebra can be computed as the least fixpoint of the operator

[figure: Sub_{H}(\overline{ω}); L; Sub_{H}(L\overline{ω}); ς^{−1} ∘ −; Sub_{H}(\overline{ω}).]

Writing 0 for the initial object, one can see that the initial L-algebra is the union of the countable diagram

[figure: 0; >; o; L0 = 1; >; Lo; L^{2}0 = Σ; >; L^{2}o; …; ,]  (1)

as it consists of all those local elements which have finite image. It follows that the union is closed under the structure map ς: \overline{ω} ^{}L\overline{ω}.

Call w the vertex of the colimit (1) and let c: w ^{}\overline{ω} be the canonical map from the initial algebra to the final coalgebra, see [3]. To check that Σ^{c} is iso, note that Σ^{w} is the limit in H of the diagram

[figure: 1 = Σ^{0}; Σ^{o}; Σ = Σ^{L0}; Σ^{Lo}; Σ^{Σ} = Σ^{L^{2}0}; Σ^{L^{2}o}; …; .]  (2)

Diagram (2) is in fact in (the image of) S(L), and since (C_{1}) is a colimit diagram, it follows by Lemma 7(i) that the limit of the diagram (2) is Σ\overline{ω} in S(L); hence also in H, by the Yoneda lemma. Therefore, Σ^{c}: Σ\overline{ω} ^{}Σ^{w} is iso.

We have established the following.

Theorem 8 The topos H with the dominance ⊤: 1 ^{}Σ is a model of the axioms of synthetic domain theory as in [8].

Remark 9 A slightly different collection of axioms, also denoting models of synthetic domain theory, appeared in the literature, see [17]. By the results therein, it follows that H with Σ is also such a model.

3 A model for the stable case

As advocated by Martin Hyland, there should be variations of the synthetic theory incorporating other models of computation. We present one such construction, similar to that of section 1 and discuss the properties it satisfies in the vein of section 2.

Let ω-St be the category of ω-complete posets with ω-continuous pullbacks (= meets of bounded pairs which distribute over sups of ω-chains) and stable (i.e. pullback preserving) ω-continuous functions.

Consider the following full subcategories of ω-St:

– the monoid L_{2} determined by the endomaps of \overline{ω} × 2,

– the category F_{2} of finite products of \overline{ω}. (F_{2} is a non-full subcategory of F.)

Since ω-continuous functions between ω-complete totally ordered sets always preserve pullbacks, the category L embeds fully into S(L_{2}) as \overline{ω} is a retract of \overline{ω} × 2.

Proposition 10 In ω-St, the object \overline{ω} × 2 is a dense generator.

Thus, we have that the “Yoneda” functor Y: ω-St ^{}Set^{L^{2}^{op}} is full and faithful, and preserves limits and exponentials.

Let H_{2} be the topos sh(F_{2}, can) of sheaves on F_{2} for the canonical topology.

Theorem 11 The inclusions

L  L_{2}  F_{2}

[figure: S(L); ∩; ⊂; S(L_{2}); ∩; ⊂; S(F_{2}); ∩]

induce

H ≃ sh(L, can) [figure: ⊥; faithful] sh(L_{2}, can)  H_{2}

[figure: sh(S(L_{2}), can); ≃; ≃; sh(S(F_{2}), can).; ≃]

PROOF. It is similar to that of Theorem 3, again using the Comparison Lemma of [9]. Also in S(L_{2}) epimorphisms are retractions, and the inverse image of a mono intersecting the image of a map is computed on the underlying set. The canonical topology can be characterized as follows.

Lemma 12 The collection of non-empty families R of monos in S(L_{2}) with common codomain D such that

(i) for every p: 2 × 2 ^{}D in ω-St there exists f ∈ R such that im(p) ⊆ im(f), and

(ii) for every unbounded countable chain ⟨x_{k}⟩ in D there exists f ∈ R such that {x_{k} | k ∈ N, x_{k} ∈ im(f)} is infinite,

is a basis for the canonical topology on S(L_{2}).

PROOF. The description is very similar to that given in Lemma 4 for the category S(L). Just observe that the first condition there can be restated as follows:

(i′) for every p: 2 ^{}\overline{ω} in ω-Cpo there exists f ∈ R such that im(p) ⊆ im(f).

The proof is also similar to that of Lemma 4.

Now use the above characterization to show that every object in S(F_{2}) is covered by the family of all maps from \overline{ω} × 2 into it, and conclude by noticing that these covers generate the canonical topology.

Analogously to Theorem 5, for D in ω-St, we have that Y (D) is a sheaf and that Y: ω-St ^{}H_{2} is a full reflective exponential ideal.

We can characterize the closure under isomorphism of the image of Y: an object F in H_{2} is (isomorphic to) Y (D) for some D in ω-St if it takes, to limit diagrams, the following six colimit diagrams: (R′), (T), (A), (C_{1}), and

[figure: 1; 1; 2; 2; 1; (⟨0, 1⟩, ⟨1, 1⟩); 2 × 2,; (⟨1, 0⟩, ⟨1, 1⟩)]  (S)

[figure: 2; (0, 2); 3; (0, 1, 3); 4; …; …; \overline{ω} + 1 ,]  (L)

where \overline{ω} + 1 is the succesor ordinal of \overline{ω}. As in section 1, the first three diagrams ensure that ⟨F 0, F 1⟩: F 2 ^{}F 1 × F 1 yields a partial order on F (1). The pullback F (S) determines F (2 × 2) as consisting of two elements with a common upper bound and a meet. Indeed, we shall prove that m = F (0, 0): F (2 × 2) ^{}F (1) is a meet of bounded pairs. Let a, b ≤ c in F (1). Then

m(a ≤ c ≥ b) ≤ a  and  m(a ≤ c ≥ b) ≤ b.

Moreover, if x ≤ b ≤ c, then

m(x ≤ c ≥ b) = x

because the diagrams

[figure: 1; 1; 2; 1; ⟨0, 0⟩; 2 × 2]
[figure: (1, 2); and]
[figure: 2; 1; 2 × 2; 2; 0; (0, 2); 3; . . . . .]

[figure: (0, 2)] ......._{}

3

commute. Finally, since 2 × 3 is covered by any sieve containing the three copies of 2 × 2 in 2 × 3, it follows that

m(x ≤ a ≥ m(a ≤ c ≥ b)) = m(x ≤ c ≥ b).

So, for x ≤ a, b we have

x = m(x ≤ c ≥ b) = m(x ≤ a ≥ m(a ≤ c ≥ b)) ≤ m(a ≤ c ≥ b).

As in section 1, the limit F (C_{1}) gives the possibility to compute sups via the map F (N): F (\overline{ω}) ^{}F (1) and, using the limit F (L), one can see that this is indeed the case. Finally, the canonical cover consisting of the family ⟨id, 0⟩: \overline{ω} ^{>} ^{}\overline{ω} × 2, ⟨id, 1⟩: \overline{ω} ^{>} ^{}\overline{ω} × 2 and all 2 × 2^{>} ^{}\overline{ω} × 2, yields the distributivity of bounded meets over sups.

The category ω-St has a representation for partial maps defined on stable open subsets. The quickest way to define these is by stating that Y (1: 1 ^{}2), denoted ⊤: 1 ^{}Σ, be the generic stable open subset in H_{2}. The algebraic way to define the notion in ω-St is as follows: an open subset U ^{⊂} ^{}D is stable if whenever a, b in U are bounded in D, then a ∧ b is in U. The representing functor adds a new element below the given order, and it is easy to see that the construction applies S(F_{2}) into itself.

Theorem 13 The topos H_{2} with the dominance ⊤: 1 ^{}Σ is a model of the axioms of synthetic domain theory as in [8], except for axioms 5 and 7.

The proof is like before. The non-valid axioms witness the fact that categories of domains like ω-St are not closed under the operation of adding a top element and that, in general, the union of stable open subsets is not a stable open subset.

We stress that missing to satisfy axioms 5 and 7 is not crucial for the synthetic theory as the core of the subject can be developed from the remaining axioms, see [14].

Acknowledgements

We thank Martin Hyland for inspiring discussions and useful comments on a preliminary version of this paper.

References

[1] A. Carboni, M.C. Pedicchio, and G. Rosolini, editors. Category Theory, Proc., Como 1990, volume 1488 of Lecture Notes in Mathematics. Springer-Verlag, 1991.

[2] M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University Press Distinguished Dissertations in Computer Science, 1996.

[3] P. Freyd. Algebraically complete categories. In Carboni et al. [1], pages 95–104.

[4] P. Freyd. Remarks on algebraically compact categories. In M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Proc. Symposium in Applications of Categories to Computer Science. Cambridge University Press, 1992.

[5] P.J. Freyd. Recursive types reduced to inductive types. In Mitchell [10], pages 498–507.

[6] P.J. Freyd and A. Scedrov. Categories and Allegories. North Holland Publishing Company, 1991.

[7] C.A. Gunter. Semantics of Programming Languages: Structures and Techniques. The MIT Press, 1992.

[8] J.M.E. Hyland. First steps in Synthetic Domain Theory. In Carboni et al. [1], pages 131–156.

[9] S. MacLane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.

[10] J. Mitchell, editor. Proc. 5^{th} Symposium on Logic in Computer Science, Philadelphia, 1990. IEEE Computer Society.

[11] P. Mulry. Generalized Banach-Mazur functionals in the topos of recursive sets. J. Pure Appl. Alg., 2:71–83, 1981.

[12] W. Phoa. Effective domains and intrinsic structure. In Mitchell [10], pages 366–377.

[13] G. Rosolini. Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986.

[14] G. Rosolini. Notes on Synthetic Domain Theory, 1994. Available from

http://hypatia.dcs.qmw.ac.uk.

[15] D.S. Scott. Data types as lattices. SIAM J. Comput., 5(3):522–587, 1976.

[16] D.S. Scott. Relating theories of the λ-calculus. In R. Hindley and J. Seldin, editors, To H.B. Curry: essays in combinatory logic lambda calculus and formalisms, pages 403–450. Academic Press, 1980.

[17] P. Taylor. The fixed point property in synthetic domain theory. In G. Kahn, editor, Proc. 6^{th} Symposium on Logic in Computer Science, pages 152–160. IEEE, 1991.

[18] G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.