Jean Yang

I am a fifth-year Ph.D. student at MIT advised by Armando Solar-Lezama. I am in the Computer-Aided Programming group.

I want to automate the tedious, error-prone aspects of programming so programmers can focus on more interesting functionality. Towards this I am interested in the interaction of declarative logical constructs with non-declarative programming models. Programming in pure logic is often useful, but not necessarily for all aspects of a problem.

For my Ph.D. thesis I am creating a programming language for automatically enforcing information flow policies for privacy. I have designed a language, Jeeves, that allows the programmer to implement rules for the flow of values separately from the rest of the functionality. The Jeeves runtime is responsible for producing outputs that adhere to the policies for protecting both reads (confidentiality) and writes (integrity). I have been developing the semantics, theoretical guarantees, and implementation. I plan to demonstrate the feasibility of this approach in web frameworks.

To get an idea of where I am coming from, you may be interested in the MIT programming languages page.

If you are wondering whether you should learn Scala, you should read my blog post on why the answer is probably yes.

Research Projects.

The Jeeves programming language for automatically enforcing privacy policies. I began working on this concept for my masters thesis ("Specification-Enhanced Executions") and I am still working on it.
The Verve operating system, the first operating system to be verified automatically and end-to-end for type safety. I worked on this during my internship at Microsoft with Chris Hawblitzel summer 2009.

Peer-Reviewed Publications.

Faceted Execution of Policy-Agnostic Programs, Thomas H. Austin, Jean Yang, Cormac Flanagan, and Armando Solar-Lezama. PLAS Workshop 2013 (to appear).
A Language for Automatically Enforcing Privacy Policies, Jean Yang, Kuat Yessenov, and Armando Solar-Lezama. POPL 2012. [Paper: pdf | Slides: pptx pdf | Talk: mp4 stream | BibTex]
Secure Distributed Programming with Value-Dependent Types, Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang. ICFP 2011. [Paper: pdf | BibTeX]
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System, Jean Yang and Chris Hawblitzel. CACM Research Highlight. Communications of the CACM, September 2010. [Full text: html pdf | Technical Perspective: html pdf | [BibTeX]
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System, Jean Yang and Chris Hawblitzel. PLDI 2010. Best paper award. [Paper: pdf | Slides: pptx pdf | Related video | BibTeX]

Press.

What your online friends reveal about where you are. Jacob Aron, NewScientist, January 25, 2012.

Awards and Honors.

Facebook Fellowship, 2012-2013.
National Science Foundation Graduate Research Fellowship, 2008-2011.

Teaching.

Programming languages research is more impactful when programmers understand how to use and evaluate their tools. Towards this goal I have designed the following courses:

Introduction to C Memory Management and C++ Object-Oriented Programming (IAP 2010).
So You've Always Wanted to Learn Haskell? (IAP 2010).

You may see my CV for a complete listing of my teaching experience.

Relevant Activities and Links.

Service.

I started the annual MIT Programming Languages Offsite Meeting in spring 2010 for the research groups in programming languages and relarted areas to exchange updates, discuss the state of the field, and discuss future directions.

I co-founded Graduate Women at MIT in fall 2009 for the promoting the personal and professional development of graduate women. One of my current projects is Positivity@MIT for creating a more positive workplace environment.

Writing.

I occasionally blog about academia and life in graduate school. I recently joined the CACM blogroll.

Advice.

I have compiled the following advice on applying to graduate school:

Other.

My brogramming project examines the "brogrammer" trope in tech culture and also society's image of the programmer. My Strong Reject meme satirizes the human aspects of the scientific reviewing process.

I discuss graduate school and computer science in Lan Li's short documentary film rocks, bands, logic (fall 2011).

If you are curious about how I came to study computer science, you may enjoy this nicely illustrated profile my classmate Julia Lindau made.