Domain theoretic denotational semantics in type theory

Tom de Jong

Denotational semantics aims to understand computer programs by assigning mathematical meaning to the syntax of a programming language in a compositional fashion. Even fairly basic programming constructs, like general recursion, require a mathematical semantics beyond ordinary sets. This leads us to a domain theoretic denotational semantics based on certain complete posets, called domains, and continuous functions between them, as pioneered by Strachey and Scott, and further refined by Plotkin and many others. This work has traditionally been carried out in classical set theory. I will talk about what goes into developing domain theory in constructive type theory, as carried out in my PhD thesis where we fix the constructive type theory to be (predicative) homotopy type theory. Moreover, I will explain how computational intuitions align rather nicely with a constructive development of domain theory. Finally, if time permits, I will briefly discuss the desire and possibility of so-called synthetic domain theory (SDT) where domains are certain sets and all functions between domains are continuous, allowing you to avoid continuity proofs at the cost of having to work constructively. A putative type theory for SDT could be seen as a specific and low dimensional instance of a directed type theory for categories.

---

Previous: Hendrik van Antwerpen | Declarative Name Binding for Type System Specifications
Next: