[TYPES] I: On Dependent types and Subtyping's consistency

[Giuseppe Castagna]

An older work in which you have a limited form of intersection types is:

G. Castagna and G. Chen: Dependent types with subtyping and late-bound 
overloading. Information and Computation, vol. 168, n. 1, pag. 1-67, 
2001. https://www.irif.fr/~gc/papers/infcomp99.pdf

and you may be also interested in

AC96b. D. Aspinall and A. Compagnoni. Subtyping dependent types. In 
Proc. 11th Annual Synposium on Logic
in Computer Science, IEEE, pages 86–97, 1996

Beppe

On 12/12/17 11:45, Gabriel Scherer wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> There is a language with dependent types and subtyping (including
> contravariant functions) in:
>
>    Normalization by Evaluation for Sized Dependent Types
>    Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017)
>    http://www.cse.chalmers.se/~abela/icfp17-long.pdf
>
> However, subtyping there is not "higher-order" in the sense of having
> type-indexed parameters themselves indicate a variance (you cannot
> abstract over all covariant parametrized types) -- pi-types only track
> relevant and irrelevant abstraction. In contrast, see the
> "higher-order subtyping" for F-omega-sub in
>
>    Polarized Subtyping for Sized Types
>    Andreas Abel, 2008
>    http://www.cse.chalmers.se/~abela/mscs06.pdf
>
>
> For higher-order subtyping in dependent systems, the two references
> I know of happen to be also mentioned on the nLab wiki:
>
>    https://ncatlab.org/nlab/show/directed+homotopy+type+theory
>
> they are the work by Harper and Licata on directed type theory (and
> Dan Licata's PhD thesis), and Andreas Nuyts' master thesis.
>
>    2-Dimensional directed dependent type theory
>    Robert Harper, Dan Licata, 2011
>    http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf
>
>    Dependently Typed Programming with Domain-Specific Logics
>    Dan Licata, 2011
>    http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf
>
>    Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance
>    Andreas Nuyts, 2015
>    http://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf
>
>
> On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami <giacomo.bergami2 at unibo.it
>> wrote:
>> [ 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/
>>