Subtyping with Singleton Types

A minimal typed lambda-calculus with singleton types and Pi-types is introduced. Some basic meta-properties are proved and it is given a PER semantics.
David Aspinall.
Subtyping with Singleton Types.
In Proc. Computer Science Logic, CSL'94, Kazimierz, Poland. LNCS 933, p.1-15, Springer, 1995.
Download as gzipped ps or gzipped dvi.

Click here to return to my papers page.

my Vcard
David R. Aspinall, email
Contact GPG key (Instant HOWTO)