[ 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
[ 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:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
An additional example is:
"Pure Subtype Systems", POPL 2010
https://dl.acm.org/citation.cfm?id=1706334
Which shows that you can combine subtyping and dependent typing into a
single relation. The PSS theory is
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Below are some additional references, that include not only subtyping and
dependent types, but also intersection types (which, in my opinion, are
important whenever subtyping is in play). There are also conference
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The software implementation described at
http://www.owlofminerva.net/files/formulae.pdf
has many similarities to your reference
http://lucacardelli.name/Papers/Dependent%20Typechecking.US.pdf
It
