The founding act of denotational semantics was Scott's model of the untyped lambda calculus, which is surely the paradigmatic dynamically typed language. Moreov

The founding act of denotational semantics was Scott's model of the untyped lambda calculus, which is surely the paradigmatic dynamically typed language. Moreover, its creation led to an immense body of work on type theory, because there are two two distinct, but related, intuitions underpinning what a type is. On the one hand, you can think of starting with some given notion of computation (the lambda-calculus, say, or x86 machine code), and then you can think of types as picking out particular subsets of the set of valid programs. (In jargon, this is "types as retracts".) In this view, a type is a property of a program. On the one hand, you can say that only things which pass type-checking are programs, and things which don't type check are simply not well-formed programs. In this view, a type is a kind of grammaticality constraint. If you don't have a model of the untyped lambda calculus, you can't speak formally about the first view, which is very limiting. This is because being able to shift between the views is important for thinking flexibly about different kinds of problems. Of course, you can also try to combine these two views. A few years back, Noam Zeilberger and Paul-Andre Mellies wrote a gorgeous paper, "Functors are Type Refinement Systems", which lays out the principles of how these two views interact. http://noamz.org/papers/funts.pdf http://noamz.org/papers/funts.pdf