[TYPES] An Expressive Type System helping for run-time verification

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

We plan to leverage expressive type systems to support the correctness
of run-time verification.
For now we are focusing on class invariants only.

We are struggling to find related works about "sound/correct" run time
verification,
in the context of pure object oriented languages.
Please, can you suggest us some reference?

Marco.

p.s.
For now, we are even struggling to define formally what should it means to
soundly enforce a (multi object) class invariant at run time, without relying on
pre-post conditions but just on the semantic of the language.