Abstract

Following last seminar talk, in order to support first-class module system in a dependently typed language, we study the coercive subtyping system for dependent types, which turns out to be challenging enough. In this talk, we show three attempts of formalizing the coercive subtyping system, each solving some problems present in the previous one.

We also study the addition of dependent intersection types to the system, which also presents some interesting challenges.