Research Statement

The goal of my research is to improve the security and reliability of software systems through the use of programming language technology. To that end, I am interested both in developing languages with more expressive type and proof systems and in enhancing and formally certifying the trustworthiness of languages and their implementations. Large software systems consist of hundreds or thousands of components, and many of these may be of uncertain origin. To ensure reliable and secure operation, it is important to defend against faulty or malicious code. Statically-typed programming languages provide facilities for information hiding—type abstraction mechanisms like existential types (the basis of abstract data types or ADTs) and parametric polymorphism— that make large-scale software development feasible by allowing programmers to write modular and secure code. If access to some private implementation detail might enable an attack, then this detail is made in-accessible by hiding it behind an abstract interface (for instance, using an existential type). The theoretical justification for this comes from relational parametricity, a strong semantic property that guarantees repre-sentation independence—i.e., that the behavior of a client (or attacker) of an ADT cannot depend on the representation and implementation details hidden behind the abstract type. Unfortunately, type abstraction does not always guarantee information hiding in practice. One issue i