Jonathan Sterling: "Synthetic Domains in the 21st Century" скачать в хорошем качестве

Jonathan Sterling: "Synthetic Domains in the 21st Century"

Topos Institute Colloquium, 28th of September 2023. ——— It is easy to teach a student how to give a naïve denotational semantics to a typed lambda calculus without recursion, and then use it to reason about the equational theory: a type might as well be a set, and a program might as well be a function, and equational adequacy at base type is established using a logical relation between the initial model and the category of sets. Adding any non-trivial feature to this language (e.g. general recursion, polymorphism, state, etc.) immediately increases the difficulty beyond the facility of a beginner: to add recursion, one must replace sets and functions with domains and continuous maps, and to accommodate polymorphism and state, one must pass to increasingly inaccessible variations on this basic picture. The dream of the 1990s was to find a category that behaves like SET in which even general recursive and effectful programming languages could be given naïve denotational semantics, where types are interpreted as “sets” and programs are interpreted as a “functions”, without needing to check any arduous technical conditions like continuity. The benefit of this synthetic domain theory is not only that it looks “easy” for beginners, as more expert-level constructions like powerdomains or even domain equations for recursively defined semantic worlds become simple and direct. Although there have been starts and stops, the dream of synthetic domain theory is alive and well in the 21st Century. Today’s synthetic domain theory is, however, both more modular and more powerful than ever before, and has yielded significant results in programming language semantics including simple denotational semantics for an state of the art programming language with higher-order polymorphism, dependent types, recursive types, general reference types, and first-class module packages that can be stored in the heap. In this talk, I will explain some important classical results in synthetic domain theory as well as more recent results that illustrate the potential impact of “naïve denotational semantics” on the life of a workaday computer scientist.