[L6] ================================================ AMAST Links 02 07

                       Subtyping Dependent Types
                 David Aspinall and Adriana Compagnoni

  We describe a subtyping extension of the Pure Type System lambdaP
(an abstract version of LF).  This system is the simplest corner of
the lambda-cube with type-dependency, yet forms the core of applied
type-theories for which subtyping is a desirable extension, for
example to give better economy of encodings in LF or to allow
automatic adaptation of proofs in \lambdaPRED (the predicate
calculus fragment of the Calculus of Constructions).

  We establish some meta-theoretic results about the system, including
subject reduction, minimal types and decidability.  

  The combination of subtyping and type-dependency is quite tricky to
analyse, mainly because the typing and subtyping relations are
mutually defined, which means that tested techniques of examining
subtyping in isolation no longer apply.  We prove our results using
an algorithmic reformulation which breaks some circularity of the
definitions, and separates beta-reduction on types and terms.

  The paper is available by ftp from Edinburgh at URL:
ftp://ftp.dcs.ed.ac.uk/pub/da/psub.ps.gz