Type Systems for Concurrency

In today's mobile world, all programs are concurrent and distributed. This challenges the traditional sequential model of computing, leading to new and hard-to-diagnose bugs such as data races and non-determinism. One central focus of my work has been to develop type systems to prevent concurrency-related bugs by construction from software.

Publications related to Type Systems for Concurrency:

• Edwin Westbrook, Jisheng Zhao, Zoran Budimlic, Vivek Sarkar. Practical Permissions for Race-Free Parallelism. Proceedings of the 26th European Conference on Object-Oriented Programming (ECOOP ’12).
• Edwin Westbrook, Jisheng Zhao, Zoran Budimlic, Vivek Sarkar. Permission Regions for Race-Free Parallelism. Proceedings of the 2nd International Conference on Runtime Verification (RV ’11).

HobbitLib, a Haskell Library for Name-Binding

Having the right data representation can vastly affect the ease with which we write programs. Unfortunately, it is difficult to build the "right" representation of programs themselves, because of constructs which bind variables, such as function definitions:

foo (int x) { ... }

HobbitLib is a Haskell library that provides a data-type for representing variable-binding constructs in programming languages. This representation satisfies the following four properties:

1. Freshness (also called "Shadowing"): foo (int x) { ... } introduces a new variable x that is distinct from any previously-bound variables, even if those were also written "x";
2. Renaming (also called "Alpha-Equivalence"): foo (int x) { ... x ... } = foo (int y) { ... y ... };
3. Scoping: variable x should not occur outside of a foo (int x); and
4. Typing: Variable x in foo (int x) { ... } should only be used as a term variable of type int.

The upshot is that any code that uses the HobbitLib representation for variable-bindings is statically guaranteed to never violate these properties, as the properties are built into the representation. This eliminates whole classes of bugs. In addition, we can use these to build representations of all and only the well-typed programs of a language, allowing us to further guarantee that all of our program-manipulating code is type-preserving.

HobbitLib can be downloaded using Haskell's cabal tool, by typing "cabal install hobbits" at a command prompt, or by using the above link.

HobbitLib and other Name-Binding Publications:

• Edwin Westbrook, Nicolas Frisby, Paul Brauner.Hobbits for Haskell: A Library for Higher-Order Encodings in Functional Programming Languages. Proceedings of the Haskell Symposium 2011 (Haskell ’11).
• Edwin Westbrook, Mathias Ricken, Jun Inoue, Yilong Yao, Tamer Abdelatif, and Walid Taha. Mint: Java Multi-stage Programming Using Weak Separability. ACM SIGPLAN 2010 Conference on ProgrammingLanguage Design and Implementation (PLDI ’10).
• Edwin Westbrook, Aaron Stump, and Evan Austin. The Calculus of Nominal Inductive Constructions. 4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP ’09).
• Edwin Westbrook. Free Variable Types. 7th Symposium on Trends in Functional Programming (TFP ’06).

Additional Projects

• Predicate monads, a compositional verification framework for monadic programs
• Specware-Coq is a plugin for Coq that allows synthesis of correct-by-construction software from high-level specifications