Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of sharp elements. Being apart is a positive formulation of being unequal, similar to how inhabitedness is a positive formulation of nonemptiness. To exemplify sharpness, we note that a lower real is sharp if and only if it is located. Our first main result is that for a large class of continuous dcpos, the Bridges–Vîţǎ apartness topology and the Scott topology coincide. Although we cannot expect a tight or cotransitive apartness on nontrivial dcpos, we prove that the intrinsic apartness is both tight and cotransitive when restricted to the sharp elements of a continuous dcpo. These include the strongly maximal elements, as studied by Smyth and Heckmann. We develop the theory of strongly maximal elements highlighting its connection to sharpness and the Lawson topology. Finally, we illustrate the intrinsic apartness, sharpness, and strong maximality by considering several natural examples of continuous dcpos: the Cantor and Baire domains, the partial Dedekind reals, the lower reals and, finally, an embedding of Cantor space into an exponential of lifted sets.

This work presents game semantics of Martin-Löf type theory (MLTT) equipped with the One, the Zero, the N, Pi, Sigma and Id types. Game semantics interprets a wide range of logic and computation, even the polymorphic $\lambda$-calculus; however, it has remained a well-known challenge in the past 25 years to achieve game semantics of dependent type theories such as MLTT, and past attempts lack directness or generality. For instance, the approach taken by Abramsky et al. interprets Sigma types indirectly by formal lists, not by games, making an interpretation of universes hopeless, and it is limited to a very specific class of dependent types. The difficulty of this challenge comes from a conflict between the extensionality of dependent types and the intensionality of game semantics. We overcome the challenge by inventing a novel variant of games, while we keep strategies unchanged, in such a way that this variant inherits the strong points of conventional game semantics. Also, our method enables an interpretation of subtyping on dependent types for the first time as game semantics. We finally give a new, game-semantic proof of the independence of Markov’s principle from MLTT. This proof illustrates an advantage of our intensional model over extensional ones such as Hyland’s effective topos.

Robinson’s unification algorithm can be identified as the underlying machinery of both C. Meredith’s rule D (condensed detachment) in propositional logic and of the construction of principal types in lambda calculus and combinatory logic. In combinatory logic, it also plays a crucial role in the construction of Meyer, Bunder & Powers’ Fool’s model. This paper now considers pattern matching, the unidirectional variant of unification, as a basis for logical inference, typing, and a very simple and natural model for untyped combinatory logic. An analysis of the new typing scheme will enable us to characterize a large class of terms of combinatory logic which do not change their principal type when being weakly reduced. We also consider the question whether the major or the minor premisse should be used as the fixed pattern.