Paper on dependent types with subtyping and overloading

To: types@cis.upenn.edu
Subject: Paper on dependent types with subtyping and overloading
From: Giuseppe Castagna <Giuseppe.Castagna@ens.fr>
Date: Fri, 21 May 1999 12:44:10 +0200
Sender: Giuseppe.Castagna@ens.fr

We would like to announce that the following paper

                    DEPENDENT TYPES WITH SUBTYPING
                      AND LATE-BOUND OVERLOADING

                                  by
                       G. Castagna and G. Chen

is available at the URL

ftp://ftp.ens.fr/pub/dmi/users/castagna/piand-ic.ps.gz

All comments will be welcome (this paper will appear in Information
and Computation. We are typesetting it in the journal format and we will 
be happy to include all interesting remarks in the published version).



                               ABSTRACT

We present a calculus with dependent types, subtyping, and late-bound
overloading. Besides its theoretical interest this work is motivated
by several practical needs that range from 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.  While
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 define here as by-product a new subtyping system for
dependent types that improves previous systems and enjoys several
properties (notably the transitivity elimination property). The
calculus with overloading is then obtained as a conservative extension
of this new system.  Another difficult point is strong normalization,
which is a necessary condition to the decidability of subtyping and
typing relations. The calculus with overloading is not strongly
normalizing. However, we show that a reasonably useful fragment of the
calculus enjoys this property, and that its strong normalization
implies the decidability of its subtyping and typing relations.

The article is divided into two parts: the first three sections
provide a general overview of the systems and its motivations, and can
be read separately; the remaining sections develop the formal study.


Giuseppe Castagna and Chen Gang