ABSTRACT. Model comparison games such as Ehrenfeucht-Fraisse, pebble and bisimulation games play a central role in finite and infinite model theory, modal logic and concurrency theory.

We show how such games can be understood in terms of comonads on the category of relational structures and homomorphisms. This leads to novel syntax-free characterizations of the equivalences induced by a wide range of logics, and coalgebraic characterizations of key combinatorial parameters such as tree-width and tree-depth.

This in turn leads to a novel analysis of back-and-forth equivalences. Instead of considering partial isomorphisms with back- and forth- extension properties, we show how they can be characterized in a uniform fashion in terms of sets of coKleisli morphisms for the associated comonads, satisfying a local invertibility condition. This leads in turn to a fixpoint characterization.

An interesting feature of this characterization is that we are approximating partial maps by (sets of) total ones, and replacing extension properties with a greatest fixpoint computation.

ABSTRACT. Differential programming, particularly systems based on Automatic Differentiation, has recently become a popular method to approach high-dimensional optimisation and integration problems found in machine learning and computational statistics. Examples of systems relying on these techniques are TensorFlow and Stan. The semantics of such systems, however, still remains rather poorly understood. In particular, it is unclear how differentiation should interact with more traditional computer science concepts like recursion. For these purposes, we are exploring a rich semantic framework for differential programming based on generalised smooth spaces known as diffeological spaces. We demonstrate how to construct Fiore's axiomatic domain theory in this setting.

ABSTRACT. Intensional computation supports generic queries of internal structure as well as the extensional computation familiar from lambda-calculus and combinatory logic. This paper introduces a denotational semantics for the simplest intensional calculus, namely SF-calculus. Its domain has a basis given by the normal forms of the calculus, extended with a least element. Their functionality is revealed by a mapping from the domain to its function space that is determined by the reduction rules of the calculus. Conversely, step-functions correspond to simple pattern-matching functions. These are representable in SF-calculus, which yields a right inverse to the mapping above. However, this semantics fails for traditional combinatory logic (SK-calculus) as the corresponding mapping into the function space does not have a right inverse. This is because combinatory logic cannot represent enough pattern-matching functions, cannot support intensional computation. This result complements the syntactic proof that SF-calculus is more expressive than SK-calculus.

ABSTRACT. I will describe ongoing work investigating a convenient category of pre-domains and a probabilistic powerdomain construction suitable for statistical probabilistic programming semantics, as used in statistical modelling and machine learning. Specifically, we provide (1) a cartesian closed category; (2) whose objects are (pre)-domains; and (3) a commutative monad for probabilistic choice and Bayesian conditioning. Jones and Plotkin have shown that conditions (2)--(3) hold when one restricts attention to continuous domains, and Jung and Tix have proposed to search for a suitable category of continuous domains possessing all three properties (1)--(3), a question that remains open to date.

I propose an alternative direction, considering spaces with separate, but compatible, measure-theoretic and domain-theoretic structures. On the domain-theoretic side, we require posets with suprema of countably increasing chains (omega-cpos). On the measure-theoretic side, we require a quasi-Borel space (qbs) structure, a recently introduced algebraic structure suitable for modelling higher-order probability theory. There are three equivalent characterisations of this category given by: imposing an order-theoretic separatedness condition on countable-preserving omega-cpo-valued presheaves; internal omega-cpos in the quasi-topos of quasi-Borel spaces; and an essentially algebraic presentation. The category of these omega-qbses validates Fiore and Plotkin's axiomatic domain theory, yielding semantics for recursive types. To conclude, I will describe a commutative powerdomain construction given by factorising the Lebesgue integral from the space of random elements to the space of sigma-linear integration operators.

ABSTRACT. The full abstractness problem was raised by Robin Milner and the diculty of designing fully abstract semantics is well-known. A denotational semantics is said to be fully abstract if it is correct and complete. The correctness condition is usually easy to establish. However, it may be difficult to establish the completeness condition. In this paper we study the abstractness of denotational models designed with continuation semantics for concurrency (CSC). Due to the interplay between denotations and continuations, the full abstractness problem seems to be even more dicult in continuation semantics. Although several papers employ continuations in the denotational design of concurrent languages, we are not aware of any full abstractness result for a concurrent language designed with continuations. Therefore we introduce a new criterion that we name weak abstractness (which is specific of the CSC technique): it preserves the correctness condition, but relaxes the completeness condition of the classic full abstractness criterion. Weak abstractness may be useful for a wide class of denotational models designed with continuations in which full abstractness is difficult (or impossible) to achieve. To illustrate this approach we present a denotational model for a simple asynchronous concurrent language designed with continuations over metric spaces. We show that this denotational semantics is weakly abstract with respect to a corresponding operational model.

ABSTRACT. Giving algebra semantics for recursive computation types in a language with effects has been an open problem. We explain how to solve it by expanding the category of cppo algebras to Fiore's category in which the maps are lax homomorphisms.

ABSTRACT. Over the history of its development domain theory has strongly influenced various developments in topology, particularly non-Hausdorff topology, and conversely topological notions and theories have significantly impacted domain theory. One might almost speak of a mathematical symbiosis. In this presentation we trace the historical development stream of various of these interfaces. We begin by highlighting sone of the significant developments concerning those topological spaces arising from equipping a dcpo with its Scott topology. Such spaces have been interesting test cases up until very recently for such topological concepts as sobriety, well-filteredness, coherence, and related topological notions.

Monotone convergence spaces are a useful topological generalization of these topological dcpo examples, as well as being generalizations of sober spaces. Just as general spaces have a sobrification, they have a monotone convergence space completion.

Another fruitful line of investigation has been exploring the relation between topological spaces and their lattices $\mathcal{O}(X)$ of open sets. For example the distributive continuous lattices resp.\ completely distributive lattices are precisely those lattices that can be represented as $\mathcal{O}(X)$ for some locally compact sober space resp.\ for some continuous domain equipped with the Scott topology. Very recent results on the Ho-Zhao problem fit into this category, as well as into the study of the Scott topology on dcpos.

Cartesian-closed categories are important for modeling higher types. This led originally to the search for cartesian-closed categories of continuous domains, but later led to more general notions of compactly generated spaces, QCB-spaces (quotients of countably based spaces), and equilogical spaces among other developments.

Connections with classical general topology arise by considering refinements of a given non-Hausdorff topology. One standard refinement is the patch topology, which adds complements of compact saturated sets to the set of open sets. The result is particularly pleasing for the stably compact spaces, for which one obtains a compact partially ordered space in the sense of Nachbin (in particular, a Hausdorff space). The continuous domains with stably compact Scott topology have powerdomains that are again stably compact. In the case of dcpos, a standard refinement of the Scott topology is the Lawson topology, which has also proved a useful topological tool.

Finally one should mention quasimetric spaces. Mike Smyth introduced a notion of completeness for such spaces that generalizes both directed completeness of dcpos and the traditional notion of completeness for metric spaces. The theory has undergone quite extensive development up to the current time.

ABSTRACT. We outline a domain-theoretic version of Skorohod's Theorem, a basic result in stochastic process theory. We state an analog of the theorem for domains, outline the proof of this result, and show how it implies the original result of Skorohod. We also propose several applications for the results.

ABSTRACT. We follow two threads in Dana Scott's mathematics to study frames in a different light. First, injectivity is an important idea. Second, relational reasoning can get at functional behavior (via, for example, approximable maps). These will permit us to situate frames in larger ambient categories in which constructions arise from the combination of injectivity and relational reasoning. In particular, the assembly of a frame comes about as being isomorphic to a sublocale \(\mathcal{Q}(L)\) of the frame of endo-relations on a given frame. We prove this by showing directly that \(\mathcal{Q}(L)\) has the universal property of the assembly.

From independent discoveries (Bruns and Lakser \cite{BL70}; Horn and Kimura \cite{HK71}), we know that frames are precisely the injective (meet) semilattices. Simply knowing this does not get us very far in studying frames \emph{qua} frames. But the full subcategory of \(\textsf{SL}\) consisting of injective semilattices comes closer. A semilattice map \(\fromto hML\) between two frames can be viewed ``approximably'' as a relation \(R_h\subseteq L\times M\) defined by \(x\leq h(y)\). Such a relation is closed under weakening: \(x\leq x'\), \(x' \mathrel{R_h}y'\) and \(y'\leq y\) implies \(x\mathrel{R_h}y\). It is a subframe of \(L\times M\). Any such relation, called a \emph{frame relation}, determines a semilattice homomorphism. So the category \(\overline{\textsf{Frm}}\) of frames and frame relations is opposite to the full subcategory of \(\textsf{SL}\) consisting of injective semilattices.

In \(\overline{\textsf{Frm}}\), an adjoint pair of morphisms, i.e., an adjoint pair of frame relations corresponds to an adjoint pair of semilattice homomorphisms. So by adjunction, the lower adjoint determines a semilattice homomorphism preserving all joins. Thus the category \(\textsf{Map}(\textsf{Frm})\), consisting of frames and adjoint pairs of frame relations \((\check f\dashv \hat f)\), is isomorphic to the category \(\textsf{Frm}\).

A subobject (a sublocale) is then an isomorphism class of extremal epimorphisms in this category. One can check that a sublocale of a frame \(L\) corresponds exactly to an idempotent, reflexive frame relation.

What we have said so far is mostly known, at least in folklore. Nevertheless, this points toward studying frames directly via frame relations, as they are (dual to) the natural morphisms of injective semilattices. To illustrate the point, we construct the assembly of a frame via frame relations, showing that its familiar universal property comes about naturally from this approach.

Between any two posets \(P\) and \(Q\), the weakening relations from \(P\) to \(Q\) obviously form a completely distributive lattice, hence a frame. If \(P\) is a meet semilattice and \(Q\) is a join semilattice, then the Heyting structure is especially easy to define; \(x\mathrel{(\Phi\to\Psi)}y\) if and only if for all \(w\) and \(z\) \(w\mathrel{\Phi}z\) implies \(w\wedge x\mathrel{\Psi} y\vee z\). One uses this to show that if \(L\) and \(M\) are frames, then the collection of all frame relations \(\overline{\textsf{Frm}}(L,M)\) is in fact a sublocale of the frame of all weakening relations. But composition of frame relations preserves only finite meets, and not arbitrary joins. So it is natural to consider the homsets as injective semilattices and not as frames, per se. Though we continue to call them frames, this suggests that we are actually studying the injective semilattice enriched category of injective semilattices.

For a frame \(L\), the frame \(\overline{\textsf{Frm}}(L,L)\) includes the reflexive, idempotent frame relations. These, as we have noted, correspond to sublocales of \(L\). Clearly, they are closed under arbitrary intersections. And a simple calculation using the Heyting arrow shows that they constitute a sublocale of \(\overline{\textsf{Frm}}(L,L)\), denoted by \(\mathcal{Q}(L)\). Moreover, \(L\) embeds in \(\mathcal{Q}(L)\) via the map sending \(a\in L\) to the frame relation \(x\mathrel{\Gamma_a}y\) if and only if \(x\leq y\wedge a\). Note that \(\Gamma_a\) corresponds to the closed sublocale of \(a\). The relation corresponding to the open sublocale is \(x\mathrel{\Upsilon_a}y\) if and only if \(a\vee x\leq y\).

Any adjoint pair \(\check f\dashv \hat f\) of frame relations between \(L\) and \(M\) extends by composition with the embedding of \(L\) in \(\mathcal{Q}(L)\) to a pair of frame relations \(f^*,f_*\) between \(\mathcal{Q}(L)\) and \(M\). These \emph{extend} \(\check f\) and \(\hat f\) in a natural way, and furthermore \(f^*;f_* \leq 1_M\). It is natural to ask when these are in fact adjoint.

The frame \(M\) has a \emph{center} relation: \(a\prec^*_M b\) if and only if there is some complemented \(w\) so that \(a\leq w\leq b\). Now if \(f=(\check f\dashv \hat f)\) is an adjoint pair of frame relations so that \(\check f;\hat f\subseteq \mathord{\prec^*_M}\), then \(f^*\dashv f_*\) is the unique adjoint pair extending \(f\) along \(\Gamma\). Conversely, using the injectivity of \(M\) and \(\mathcal{Q}(L)\), if \(f^*\) is adjoint to \(f_*\), then \(\check f;\hat f\subseteq \mathord{\prec^*_M}\). Hence, \(\mathcal{Q}(L)\) has the universal property that any adjoint pair of frame relations from \(L\) to \(M\) that sends \(L\) to the center of \(M\) factors uniquely through \(\Gamma\).

\begin{references}{99}

\bibitem{BL70} Bruns, G. and Lakser, H. Injective hulls of semilattices. \emph{Canadian Mathematics Bulletin}, \textbf{13} (1970), 115--118. \bibitem{HK71} Horn, A. and Kimura, N. The category of semilattices. \emph{Algebra Universalis}, \textbf{1} (1971), 26--38.

\end{references}

ABSTRACT. The importance of, on the one hand, categories of relations and, on the other hand, Stone Duality does not seem to be in need of much justification in a workshop on domain theory. The purpose of this presentation is to explain how both can be combined. In other words, given a concrete duality in which arrows are structure preserving functions, extend this duality to a duality of the corresponding categories of relations (Thm 1). We will use this approach to give a reconstruction of domain logics for non-zero dimensional spaces (Thm 2), based on Scott's idea of moving from algebraic to continuous lattices by splitting certain idempotents.

ABSTRACT. We study interaction between de Groot duality and the semantic domains of various choices (i.e. powerlocale constructions) on stably compact locales. We give a simple point-free account of the duality on several powerlocale constructions. This is done via the representation of a stably compact locale by means of Scott’s entailment relation with an idempotent relation due to Coquand and Zhang [Theoret. Comput. Sci., 305(1-3):77–84, 2003].