[ 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.
