[TYPES] Formal models of python-like languages

[Halley Young]

Hi all,

I have had trouble finding formal research regarding languages with all or
most of the properties of core python.  Python has the following properties:

1. It is often used in a purely imperative style, and has side effects and
pointers.
2. Functions are first class variables, and can be higher-order or
anonymous.
3. One can define objects with subclasses and inheritance, but not
everything is wrapped in a class.
4. There is dynamic "duck typing," and branches based on runtime checks of
types.

Even though obviously research on any one of these properties exist,
research on languages combining them all, or even just programming with
side-effects/pointers and higher order functions, seem to be much rarer.
Do you know of any work that has been done formalizing languages with all
or most of these features?

Thank you,
Halley Young