In (hyper)coherence semantics, proofs/terms are cliques in (hyper)graphs. Intuitively, the vertices represent the results of computations and the edge relation witnesses the ability to carry out the computation assembled into a single piece of data or a single (strongly) stable function, at arrow types.

In (hyper)coherence semantics, the argument of a (strongly) stable functional is always a (strongly) stable function. As a consequence, compared to the relational semantics where there is no edge relation, some vertices are missing. Recovering these vertices is essential if we are to reconstruct proofs/terms from their interpretations. It will also be useful for comparing with other semantics, such as game semantics.

Bucciarelli and Ehrhard (2001) introduced a non-uniform coherence space semantics, where no vertex is missing. By constructing the co-free exponential, we get a new version of this semantics, together with non-uniform versions of hypercoherences and multicoherences. This provides a new semantics in which an edge is a finite multiset. Thanks to the co-free construction, these non-uniform semantics are deterministic in the sense that the intersection of a clique and an anti-clique contains at most one vertex, which is a result of interaction, and they then extensionally collapse onto the corresponding uniform semantics.

We generalise the construction of the formal ball model for metric spaces due to A. Edalat and R. Heckmann in order to obtain computational models for separated -categories. We fully describe -categories that are

1. (a) Yoneda complete

2. (b) continuous Yoneda complete

1. (a) a quasi-metric space X is Yoneda complete if and only if its formal ball model is a dcpo, and

2. (b) a quasi-metric space X is continuous and Yoneda complete if and only if its formal ball model BX is a domain that admits a simple characterisation of approximation.

Game semantics describe the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterise definable strategies, that is, strategies that actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. In this paper we present an original methodology to achieve this task, which requires a combination of advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model using generators and relations: these strategies can be generated from a finite set of atomic strategies, and the equality between strategies admits a finite axiomatisation, and this equational structure corresponds to a polarised variation of the bialgebra notion. The work described in this paper thus forms a bridge between algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanised analysis of causality in programming languages.

Noether classes of posets arise in a natural way from the constructively meaningful variants of the notion of a Noetherian ring. Using an axiomatic characterisation of a Noether class, we prove that if a poset belongs to a Noether class, then so does the poset of the finite descending chains. When applied to the poset of finitely generated ideals of a ring, this helps towards a unified constructive proof of the Hilbert basis theorem for all Noether classes.

The purpose of this paper is to develop the basic theory of stably compact spaces (viz. compact, locally compact, coherent sober spaces) and introduce in an accessible manner and with a minimum of prerequisites some significant new lines of investigation and application arising from recent research, which has arisen primarily in the theoretical computer science community. Three primary themes have developed:

1. (i) the property of stable compactness is preserved under a large variety of constructions involving powerdomains, hyperspaces and function spaces;

2. (ii) the underlying de Groot duality of stably compact spaces, which finds varied expression, is reflected by duality theorems involving the just mentioned constructions; and

3. (iii) the notion of inner and outer pavings is a useful and natural tool for such studies of stably compact spaces.