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.