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
3:30pm
Wean 8220