[TYPES] I: On Dependent types and Subtyping's consistency
giacomo.bergami2 at unibo.it
Tue Dec 12 04:57:03 EST 2017
I am trying to check if it is possible to do reflection (as in Java) using "type safe" languages and, therefore, I am wondering if there is a language having dependent types with subtyping (in particular, I'm not talking of subtyping as in types' universes, but as in record subtyping). All the infos I got was a paper by Luca Cardelli dated 2000/2001 but, since then, it seems that whether the type system is consistent or not is still an open problem ( http://lucacardelli.name/Papers/Dependent%20Typechecking.US.pdf ).
Therefore, I'm wondering if there are any advances on this regard: moreover, it seems to be that no proof assistant supports this technology.
Thanks in advance for any reply,
University of Bologna
More information about the Types-list