[Prev][Next][Index][Thread]

paper: Subtyping Dependent Types


Hello all,

I'd like to announce the availability of a draft paper:

                       SUBTYPING DEPENDENT TYPES

                 David Aspinall and Adriana Compagnoni

  		      David.Aspinall@dcs.ed.ac.uk
	            Adriana.Compagnoni@cl.cam.ac.uk

  Abstract:

  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:

  ftp://ftp.dcs.ed.ac.uk/pub/da/psub.ps.gz

or via my home page (see below).

Adriana and I would welcome any comments or suggestions on the
contents.

  - David.


------------
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