I found two interesting review essays on domain theory in last year’s newsletter of the British BCS-FACS Formal Methods Group:
- Monahan, [2021] “Domain Theory - Revisited”
- Winskel, [2021] “Domain theory and interaction”
The first essay by Monahan gives an overview of the motivation, context of emergence and basic ideas of domain theory. He talks about overcoming distrust of the untyped lambda calculus, finding ways to scale and approaches to program specification, and the need to work with partial functions (due to general recursion).
The key idea of the domain theory is that LC functions correspond to mathematical functions over special sets (actually, domains, which model types), ordered by the amount of abstract information contained in them, and the functions preserve this order. Such a structure of functions allows us to construct fixed points for them, and thus to model recursion as the limit of the information-accumulating process. In this way, for the first time, a topological view of computation was constructed, and computer science (more precisely, the theory of programming languages) turned out to be a full-fledged mathematical theory, not just “bit shuffling”, which in turn led to the development of type theory and formal semantics.
Winskel’s essay is more technical, focusing on the topic of competitive and interacting computation. He starts with an introduction to the history of DT from the point of view of its creators, mentions the appearance of LCF/PCF and ML, then moves on to the classical problems of DT - dealing with non-determinism, the problem of complete abstraction (constructs in the model for which there is no syntax). Attempting to solve these problems, domain theory (and denotational semantics in general) moved to the creation of interactive models, further formalized in the form of game semantics. On the other hand, due to problems with competitive programs, some researchers switched to CCS/CSP process algebras with synchronization. Meanwhile, continued work in the framework of order theory led to the notion of event structure (whose formalization in Coq, by the way, can be found here).
The essay further emphasizes the connections with category theory - presheaves, monoidal categories, touches on connections with Girard’s work, describes the emergence of game semantics and its competitive variety - where both games (type models) and strategies (program models) are described by event structures (in contrast to classical tree games), shows how competitive games can be reduced to domain models, interaction geometry and lenses.