[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
I think that Monitoring-oriented programming (MOP) Framework is a strong related approach, even if it is not directly based on type systems. MOP is developed by FSL research group at UIUC led by Grigore Rosu: http://fsl.cs.illinois.edu/index.php/MOP MPOP is a part of a more complex project devoted to run-time verification: http://fsl.cs.illinois.edu/index.php/Runtime_Verification Dorel On 16/12/2017 04:15, Marco Servetto wrote:
[ 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.
