## 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

Noon

Wean 8220