A run-time monitor is a program that executes in parallel with an untrusted application and examines actions from the application's instruction stream. If the sequence of program actions deviates from a specified security policy, the monitor transforms the sequence or terminates the program. We present the design and implementation of a language called Polymer for defining the policies enforced by program monitors. One of the unique aspects of Polymer is that it provides a number of facilities for composing complex policies from simpler ones. For example, it allows policies to be parameterized by values, or other policies. There are also operators for forming the conjunction and disjunction of policies. These features allow security architects to design modular, well-structured security policies for untrusted applications written in Java.

Joint work with Lujo Bauer and Jay Ligatti.

Polytypic programming is a framework for automatically deriving functions such as marshaling, iteration, and equality based on static type information. Intensional type analysis is a similar mechanism for defining such functions, although it is based on run-time analysis of type information. However, there are a number of polytypic operations, such as iteration, that cannot be defined with traditional frameworks of run-time type analysis. These operations must be defined over higher-order type constructors, not types. In this talk, I will show how to extend intensional type analysis to type constructors so that we may define these operations. Furthermore, I will show how this extension may be done in a type-erasure framework, by using term functions to represent type constructors.

XML data are described by types involving regular expressions. This raises the question of what a convenient language feature is to manipulate such data. Previous proposals for XML processing languages such as XSLT and XQuery typically provide a ``for each'' loop construct. However, it only permits the independent processing of each children node and has no way to exploit the full structure of regular expressions. In this paper, we propose a novel programming feature regular expression filters. This construct stems from our previous proposal, regular expression pattern matching, which is inspired by the corresponding ML-style construct. We extend it by allowing pattern clauses to be closed under arbitrary regular expression operators, yielding a significat expressiveness. In particular, a clause closed by a Kleene star can iterate on sequences with no need to write an explicit recursion. In addition, we equip a typing inference mechanism that obtains (1) types for pattern variables that are locally precise with respect to the type of input values and (2) a type for the result of the whole filter expression that is also locally precise with respect to the types of the body expressions. We discuss how our construct is useful in the practice of XML processing and, in particular, how our type inference is crucial when type evolution is involved.

Most programming languages adopt static binding, but for distributed programming an exclusive reliance on static binding is too restrictive: dynamic binding is required in various guises. Typically it is provided only by ad-hoc mechanisms that lack clean semantics.

In this work we adopt a more foundational approach, showing how core dynamic rebinding mechanisms can be added to a CBV lambda-calculus. To do so we first explore refinements of the CBV reduction strategy with delayed instantiation, the _redex-time_ and _destruct-time_ semantics. Delayed instantiation is required to obtain the most recent version of a definition following a rebinding.

The destruct-time semantics gives the basis for a _lambda-mark_ calculus that supports dynamic rebinding for marshalling and unmarshalling, with primitives to package values and _marks_ to control which identifiers are dynamically rebound when they are unpackaged. We give examples in an extended lambda-mark showing how wrappers for communicating and encapsulating untrusted code can be expressed.

Finally, we use the destruct-time semantics also as a basis for a _lambda-update_ calculus with simple primitives to provide type-safe, dynamic updating of code. We thereby put a variety of real-world mechanisms on a common semantic foundation.

Joint work with Gavin Bierman, Peter Sewell, Gareth Stoyle, and Keith Wansbrough, University of Cambridge.

Global computing (WAN programming, Internet programming) distinguishes itself from local computing (LAN computing) by among other things the fact that it exposes the network to the application, rather than seeking to hide it with network transparency as in LAN programming. Global computing languages seek to provide useful abstractions for building applications in such environments. This talk gives an overview of the pik-calculus, a calculus for asynchronous distributed programming that incorporates abstractions for building fault-tolerant global applications. The calculus incorporates notions of atomic failure and failure dependencies, from which various forms of distributed transactions and optimistic computation may be built. The pik-calculus extends the asynchronous pi-calculus with a notion of logs and ``safe'' operations for modifying those logs.