Steve Zdancewic

A Syntactic Account of Type Abstraction

A variety of systems, such as web-browsers, databases, and operating systems, rely upon type-safe programming languages to support extensions (applets, for example). The accepted wisdom is that we can use abstract data types (ADTs) to prevent malicious or faulty applets from directly accessing data -- instead, the applet must pass through the interface of the ADT and hence its access can be controlled by the underlying system.

In idealized languages, such as the polymorphic lambda calculus, we can use semantic models to prove such theorems about applets, following the pioneering parametricity work of Reynolds. But these semantic arguments do not seem to scale up to languages such as Java, ML, or TAL which provide important features that are difficult to model, such as references, polymorphic equality, recursive types, objects and threads.

This talk will describe some ongoing research into using syntactic, as opposed to semantic, arguments to prove that the behavior of applets is suitably constrained by ADTs. The hope is that, as with type-soundness proofs based on subject-reduction, these syntactic arguments will scale up to realistic programming languages.

The key innovation in our approach is to use "colors" to distinguish host code from applet code during evaluation, and to use different typing rules for different colors. In particular, applet code is required to respect the abstract types of hosts throughout evaluation. We generalize this scenario to an arbitrary number of applets and hosts and show how to prove interesting properties about these interacting agents.

This is joint work with Dan Grossman and Greg Morrisett.

November 6, 1998
Wean 8220