[TYPES] Objects in type theory

[Tim Sweeney]

Hickey's 1996 "Formal Objects in Type Theory using Very Dependent Types" (
http://www.cs.cornell.edu/jyh/papers/fool3/paper.pdf) laid an interesting
type theoretical foundation for object oriented programming constructs.

I'm seeking references on any later work in this direction.  Of particular
value would be papers that explore the following:

1. Referencing superclass fields in derived classes.  E.g. A Java
programmer might create a class with a member function like "void
updateObject() {updateNewThings(); super.updateObject();}".  I can't see
how to patch this on top of Hickey's framework without losing the
straightforward classes-as-types mapping.

2. Virtual classes (https://en.wikipedia.org/wiki/Virtual_class).  Perhaps
F-bounded polymorphism comes to the rescue.

3. Ensuring open-world forward-compatibility across modules.  Java and C#
define a broad set of ways that a given module may evolve without breaking
compatibility with existing code in other modules which reference it. For
example, one may safely add a new member function to a class.  The
supporting subtyping mechanisms are well-understood, but naming and
disambiguation are required too.

Thanks,

Tim Sweeney