Paper on a type system for security

We would like to announce the availability of a draft paper on
adding security information to types in the typed lambda calculus:

    Title: The SLam Calculus: Programming with Secrecy and Integrity
    Abstract: The SLam calculus is a typed lambda-calculus that
    maintains *security information* as well as type information.  The
    type system propagates security information for each object in
    four forms: the object's creators and readers, and the object's
    *indirect* creators and readers (i.e., those agents who, through
    flow-of-control or the actions of other agents, can influence or
    be influenced by the content of the object).  We prove that the
    type system prevents security violations and give some examples of
    its power.

The paper is available from the Web page


or more directly from


Comments are most welcome.

-Nevin Heintze
 Jon G. Riecke