[ 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 implements the Type:Type rule (cf. p. 11), hence, provides an unstratified type system, has subtypes similar to the predicate subtypes in PVS (see: http://www.csl.sri.com/papers/cade92-pvs/cade92-pvs.pdf, p. 2), and a mechanism to preserve the type dependencies within the type symbol similar to the de Bruijn indices, but used for type variables within the type information only, such that no explicit type inference rules are required, but the type directly results from lambda conversion (or lambda application). Mathematical entities may have different types (i.e., it is a Curry-style rather than a Church-style system). Kind regards, Ken Kubota ____________________ Ken Kubota http://doi.org/10.4444/100 > Am 12.12.2017 um 10:57 schrieb Giacomo Bergami <giacomo.berga...@unibo.it>: > > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] > > Hello Everyone, > > 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, > > Giacomo Bergami > Ph.D Student > University of Bologna > https://jackbergus.github.io/