Abstract

In our last talk, we presented the idea of unified subtyping, which tracks typing for subtyping relations. We further studied the type system with top types and improved the non-deterministic rules for top types. We resolve the circular dependency of the metatheory by breaking the reflexivity lemma into two sub-lemmas. The result is a calculus called \I_<: (lambda-I-sub) that extends \I with subtyping. A case study of encoding purely functional objects in \I_<: shows the expressiveness of the calculus.