We developed a theory of permissions that supports delegation-based reuse, as opposed to the inheritance-based reuse present in earlier versions of Plaid. This model is both cleaner and more flexible. The model was published in FTfJP '15.

We developed a model of statically-typed object-oriented languages that support dynamic creation of class hierarchies, including mixin composition, along with a match construct that generalizes instanceof checks and casts. We started with an extensible tag construct motivated by type theory, and adapted it to support static reasoning about class hierarchy and the tags supported by each object. The implementation of the Wyvern language leverages this theory. This work was published in ECOOP '15. 

We carried out a series of three studies evaluating the concrete benefits of the documentation and checking that is enabled by that paradigm. One study appeared in ECOOP '14 and the other's are in ICPC '15. The results strongly suggest that protocols represent significant barriers in real-world developer tasks, and that interventions related to Plaid's typestate checking system and supporting documentation can significantly improve performance on these tasks.

We revised our Gradual Typestate paper (ECOOP '11) for journal publication and it has been published in ACM TOPLAS. This work investigates a theory that provides run-time support for typestate and permissions, allowing a flexible mix of static and dynamic checks to ensure that the program is safe. Our revision work has focused on refining the core model of the language, more cleanly separating out the core static theory from the extensions necessary to provide gradual typechecking. This should solidify the foundations of permission-based languages (especially Plaid) while also opening the door to more general future research mixing static and dynamic checking for permissions.

We published a description of ÆMINIUM, the concurrent-by-default extension of Plaid, at ACM TOPLAS. ÆMINIUM expresses dependencies using permissions, which are used by the type system to automatically parallelize the application. The ÆMINIUM approach provides a modular and composable mechanism for writing concurrent applications, preventing data races in a provable way.

We developed a substructural type system outfitted with a novel lightweight interference control mechanism, rely-guarantee protocols, that enables controlled aliasing of shared resources. By assigning each alias separate roles, encoded in a novel protocol abstraction in the spirit of rely-guarantee reasoning, our type system ensures that challenging uses of shared state will never interfere in an unsafe fashion. In particular, rely-guarantee protocols ensure that each alias will never observe an unexpected value, or type, when inspecting shared memory regardless of how the changes to that shared state (originating from potentially unknown program contexts) are interleaved at run-time. This work was published at ECOOP '14.
We developed a modular verification approach based on the novel abstraction of object propositions, which combine predicates and information about object aliasing. In our methodology, even if shared data is modified, we know that an object invariant specified by a client holds. Our permission system allows verification using a mixture of linear and nonlinear reasoning. We thus offer an alternative to separation logic verification approaches. Object propositions can be more modular in some cases than separation logic because they can more effectively hide the exact aliasing relationships within a module. We validate the practicality of our approach by verifying an instance of the composite pattern. We implement our methodology in the intermediate verification language Boogie (of Microsoft Research), for the composite pattern example. This work was published in the Inte...

Please report errors in award information by writing to: awardsearch@nsf.gov.