[TYPES] On Dependent types and Subtyping's consistency

[Ken Kubota]

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.bergami2 at 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/