In 1969, Dana Scott wrote an unpublished manuscript in which he said untyped lambda calculus had no mathematical meaning, 11 years later he wrote a paper that organized many of the different semantics he and others had since found using the language of category theory.

This latter paper is really the first deserving of the title “categorical semantics of dynamic typing”, and so I’m going to present some of the theorems and “theorems” presented in that paper, but mingled with the history of the idea and the preceding papers that led to them.

My Full Notes continue the story, and you might also be interested in the discussion during the lecture.