Controlled Sharing: Programming-Language Principles and Techniques

In programming languages, unforgetable references often serve as capabilities; for instance, a reference to an object may serve as a capability for accessing the object. This project studies the principles of those capabilities and develops capability-based techniques. Process calculi (in particular, relatives of the pi calculus) provide a rich, useful foundation for this work; the project investigates an extension of the pi calculus that permits operations on capabilities. In that setting, it aims to develop type systems, logics, semantics, and applications.
Several related "packaging" constructs, such as objects and abstract data types, also support controlled sharing. This project aims to advance research on these constructs and on the corresponding type structures. In particular, it explores refinements of abstract data types that guarantee representation uniformity, with logical foundations (such as Hilbert's choice operator), in the context of dynamically extensible systems. In another direction, this project studies correctness requirements on the implementations of these constructs.
Further, locking and other run-time mechanisms can impose protocols and policies for access to shared resources. This project also pursues research on disciplines for the safe use of these run-time mechanisms, and on the enforcement of these disciplines through static analysis.
Security is one of the main motivations and applications for controlled sharing. From an educational perspective, it also provides a legitimate and compelling motivation for introducing students to the programming-language concepts and techniques that are the focus of this work. Thus, security offers one of the main avenues for impact
for this project.