Subtyping Dependent Types

A subtyping extension of the type system lambdaP is proved to have decidable type-checking and subtyping problems. Includes full proofs.
David Aspinall and Adriana Compagnoni.
Subtyping Dependent Types.
Appears in TCS, 2001. Download as dvi, gzipped ps or pdf.

This also appears as the technical report ECS-LFCS-97-370 . (The version here may supersede the technical report version).




Click here to return to my papers page.

my Vcard
David R. Aspinall, email david.aspinall@ed.ac.uk.
Contact GPG key (Instant HOWTO)