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

[Frank Pfenning]

Below are some additional references, that include not only subtyping and
dependent types, but also intersection types (which, in my opinion, are
important whenever subtyping is in play).  There are also conference papers
about each of these lines of research, but by necessity they tend to be
less tutorial.

Joshua Dunfield, A Unified System of Type Refinements
<http://www.cs.cmu.edu/~joshuad/papers/thesis/>, PhD Thesis, CMU, August
2007.

William Lovas, Refinement Types for Logical Frameworks
<http://www.cs.cmu.edu/~wlovas/papers/wjl-thesis-final.pdf>, PhD Thesis,
CMU, September 2010.

Joshua combines subtyping, intersection, union, and dependent types in a
single language.  There is also an implementation of an ML subset called
Stardust (not sure about its current status).  Soundness here is not at all
obvious; there are some traps that must be avoided.  In this regard, see
also Davies & Pfenning, ICFP 2000.

William combines pure dependent types and intersection types and derives
from that a principled notion of subtyping appropriate for a logical
framework.  Here, the key is to respect the open-endedness of logical
framework specifications.

  - Frank

On Tue, Dec 12, 2017 at 4: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/
>



-- 
Frank Pfenning, Professor and Head
Department of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3891

http://www.cs.cmu.edu/~fp
+1 412 268-6343
GHC 7019