Join Us!

Our group mission is to take over the entire world with sound reasoning and provable guarantees. 🌈

You may read more about our research group and active projects here.

As I am on leave during the 2018-2019 academic year to start a Bay Area-based company to help companies get back in control of their data, we are not looking for new group members at the moment.

Programming Languages at Carnegie Mellon

CMU has a large and active Principles of Programming group. The group has become even larger and more active now that Jan Hoffmann, Matt Fredrikson, and I have joined. The School of Computer Science PhD application is here.

Research Agenda

Research projects include, but are not limited to, the following.

Factoring Privacy and Security Out of Programs

Information leaks often occur because conditional access checks are intertwined with other functionality. We want to make software more secure by reducing opportunities for programmers to inadvertently leak information. Our prior work on the Jeeves programming language introduced the idea of policy-agnostic programming: separating privacy and security policies from the rest of the code while relying on the compiler/compile to implement policy checks. Jeeves enforces policies at runtime. Follow-up work on Lifty uses a static program repair-based approach for inserting the necessary conditional checks at compile-time, where the programmer specifies policies as refinement types. We are interested in, among other things, the following extensions of this work:

• Supporting policy-agnostic programming for legacy code.
• Policy-agnostic programming for statistical privacy.
• Extending these ideas to other domains, for instance resource usage.
• Conducting realistic case studies, for instance on health record systems.

Exploiting Structure to Analyze Rule-Based Biological Models

Understanding the mechanisms behind cellular signalling would help us understand and cure many diseases, but the complexity of cellular signalling precludes understanding. We are interested in developing language constructs and programming tools for modeling cellular signalling as programs. Our work on executable knowledge exploits a deep connection between programming language semantics and semantics to support a new way of modeling. We use Kappa, a rule-based graph-rewrite programming language that allows us to encode possible transformations over graphs representing the state of the cell. Kappa's precise operational semantics allow us to not only simulate the programs, but also perform static program analysis. We are currently working as part of the Big Mechanism project to mine models from the literature. Below are some project directions.

• Formal methods techniques and tools for exploring a space of possible models.
• Tools for analyzing causal relationships between rules.
• Statistical analyses for answering questions about rules and rates.
• Applications of rule-based modeling and causal analysis in traditional Computer Science domains.

Applying to Graduate School

I have compiled the following advice on applying for a PhD in computer science:

1. Deciding to Apply
2. Standardized Tests
3. Fellowships
4. Applications
5. School Visits
6. Some notes on picking grad schools/advisors
7. FAQ: Applying to Graduate School for Computer Science

Life in Academia

If you are considering a stint in academia, you may be interested in these blog posts I have written.

Reasons to Pursue a Ph.D.	December 11, 2011
The Life of an Academic, Explained	February 5, 2012
How Science Really Works	January 12, 2013
What My PhD Was Like	February 27, 2016

Why Pittsburgh Is the Place to Be

Pittsburgh is not just affordable and liveable, but also newly hip 🔥. Why wouldn't you want to be here?

Pittsburgh Gets a Tech Makeover	July 22, 2017
A Revitalized Pittsburgh Suggests the President Used a Rusty Metaphor	June 2, 2017
Built on Steel, Pittsburgh Now Thrives on Culture	April 12, 2017
36 Hours in Pittsburgh	July 15, 2015