Subtyping with Power Types (Summary version)

A predicative type system with power types is introduced and studied, based on a reformulated fragment of Cardelli's 1988 system. It allows better logical encodings than in LF or LF with subtyping (LambdaPsub), and can express higher-order subtyping without needing special rules for operators. A particular novelty is the auxiliary system for "rough typing", which assigns simple types to terms of the calculus. This allows a model definition to be given which uses a set-theoretic containment semantics without recourse to a universal domain.
David Aspinall.
Subtyping with Power Types.
In Proc. Computer Science Logic, CSL 2000, Fischbachau, Germany. LNCS 186, p.156-171, Springer, 2000.
Download as gzipped ps or pdf.
Also available: a draft long version (ps)

Click here to return to my papers page.

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