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

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