[ 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 <[email protected]>:
>
> [ 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/
