Nevin Heintze and Jon Riecke

Security, Dependency and Regions

The talk will be in two parts. The first part (by Nevin) will start with a discussion of information flow and the SLam Calculus. We will then show that some of the structural properties of the SLam Calculus are common to other program analyses such as partial evaluation, program slicing, and call-tracking. In particular, there is a central notion of dependency that is common to all of these settings. We make this connection precise via the Dependency Core Calculus (DCC), a small extension of Moggi's computational lambda calculus.

The second part (by Jon) will describe a semantics of the region calculus of Tofte and Talpin, a typed lambda calculus that can statically delimit the lifetimes of objects. We will show how to translate this calculus into an extension of the polymorphic lambda calculus called F_#. We will give a denotational semantics of F_#, and use it to give a simple and abstract proof of correctness of memory deallocation.

A common thread of both talks is the use of logical relations.

This is joint work with Martin Abadi (Compaq) and Anindya Banerjee (Stevens Institute of Technology).

February 12, 1999
Wean 8220