LFCS
3pm Tuesday 8th July 2008
Room 4.31, Informatics Forum
Note nonstandard time
This talk is a short summary of the work in my PhD thesis. I present a novel approach to type theory called ``pure subtype systems'', and a core calculus called Deep which is based on that approach.
Pure subtype systems eliminate the distinction between types and objects; every term can behave as either a type or an object depending on context. A subtype relation is defined over all terms (both types and objects), and subtyping, rather than typing, forms the basis of the theory. We show that higher-order subtyping with bounded quantification is strong enough to completely subsume the traditional type relation.
The Deep calculus applies these concepts to the design of an advanced module system. Modules in Deep are first-class, recursive, and dependently typed. Unlike other module systems, both type and object definitions use late binding. Late binding for types makes it possible to extend a set of mutually recursive type definitions with inheritance, which means that Deep can easily solve the well-known ``expression problem.''
The cost of using pure subtype systems lies in the complexity of the metatheory. We formulate the subtype relation as a reduction system, and show that transitivity elimination (and thus type safety) follows from a confluence property of the reductions. We are able to show that the system is locally confluent, but we have not yet been able to show that it is globally confluent.