Sciweavers

Share
POPL
2010
ACM

Pure Subtype Systems

9 years 6 months ago
Pure Subtype Systems
This paper introduces a new approach to type theory called pure subtype systems. Pure subtype systems differ from traditional approaches to type theory (such as pure type systems) because the theory is based on subtyping, rather than typing. Proper types and typing are completely absent from the theory; the subtype relation is defined directly over objects. The traditional typing relation is shown to be a special case of subtyping, so the loss of types comes without any loss of generality. Pure subtype systems provide a uniform framework which seamlessly integrates subtyping with dependent and singleton types. The framework was designed as a theoretical foundation for several problems of practical interest, including mixin modules, virtual classes, and feature-oriented programming. The cost of using pure subtype systems is the complexity of -theory. We formulate the subtype relation as an abstract reduction system, and show that the theory is sound if the underlying reductions commute...
DeLesley S. Hutchins
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors DeLesley S. Hutchins
Comments (0)
books