A dependently typed calculus with polymorphic subtyping. - Mingqi Xue; Bruno C. d. S. Oliveira (Sci. Comput. Program., 2021)