Dependent types with subtyping and late-bound overloading

We present a calculus with dependent types, subtyping, and late-bound overl oading. Besides its theoretical interest this work is motivated by several practical needs that range form the definition of logic encodings to proof specialization and reuse and to object-oriented extension of the SML module system. The theoretical study of this calculus is not straightforward. Whi le confluence is relatively easy to prove, subject reduction is much harder . We were not able to add overloading to any existing system with dependent types and subtyping, and prove subject reduction. This is why we also defi ne here as by-product a new subtyping system for dependent types that impro ves previous systems and enjoys several properties (notably the transitivit y elimination property). The calculus with overloading is then obtained as a conservative extension of this new system. Another difficult point is str ong normalization, which is a necessary condition to the decidability of su btyping and typing relations. The calculus with overloading is not strongly normalizing. However, we show that a reasonably useful fragment of the cal culus enjoys this property and that its strong normalization implies the de cidability of its subtyping and typing relations. The article is divided in to two parts: the first three scetions provide a general overview of the sy stems and its motivations and can be read separately; the remaining section s develop the formal study. (C) 2001 Academic Press.