paper: Subtyping Dependent Types
Subject: paper: Subtyping Dependent Types
From: David Aspinall <email@example.com>
Date: Sun, 06 Aug 1995 14:55:50 +0100
I'd like to announce the availability of a draft paper:
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 as:
or via my home page (see below).
Adriana and I would welcome any comments or suggestions on the
David Aspinall, email: David.Aspinall@dcs.ed.ac.uk
Department of Computer Science, URL: http://www.dcs.ed.ac.uk/home/da
University of Edinburgh, Tel: +44 131 650 5898
King's Buildings, Fax: +44 131 667 7209
Edinburgh. EH9 3JZ