[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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
