The premier league of denotational semantics

Here is a list of my all-time favourite denotational semantics (in no particular order). Next to each one, I have written what I consider to be the ideal language to study it as a model of. All of these semantics are junk-free and fully abstract, but more than that, they all give a deep insight into the language. I regard them all as "discovered" rather than manufactured.
Model Language
Cpo semantics Call-by-push-value with recursion and type recursion, parallel-or and parallel-exists.
Lower powerdomain semantics Affine call-by-push-value with recursion, type recursion and erratic choice. Terms ordered by may-testing.
Pointer game semantics Non-return calculus with recursion, type recursion and higher-order storage. There's no "ref" type constructor, but the context has a separate zone for identifiers bound by new.
Sequential algorithms Affine call-by-push-value with recursion, type recursion, and control operator at ground type only.
Jonsson's infinite trace semantics for dataflow A nondeterministic dataflow language.
Paul Blain Levy