Edward Z. Yang

ezyang@
mit.edu
cs.stanford.edu
Second year PhD student at Stanford University
Massachusetts Institute of Technology 2012
University of Cambridge 2011 (CME)
RésuméCurriculum VitaeScholar
BlogTwitterG+FBTumblrGitHubLP

I am a second year PhD student at Stanford advised by David Mazières and John Mitchell. I am a proud member of the Secure Computer Systems group. I'm interested in applying operating system mechanisms (hardware isolation, dynamic resource limits) to the design and construction of programming languages, and vice versa (type systems, formal verification, information flow control). I'm a big fan of Haskell, a non-strict purely functional language.

(I use a ThinkPad X61 Tablet. Find me on freenode as ezyang, or on Strava, Stack Overflow, Wikipedia, Tripit, Reddit, LinkedIn, Mendeley.)

What are my collaborators and I working on?

Breaking barriers

Abstraction is a fundamental tenet of software engineering, and it is often enforced through mechanisms such as information hiding. For large software projects, such facilities are considered essential; for security abstractions, this enforcement is mandatory. However, real software engineers repeatedly and profitably violate abstraction: languages that are too inflexible to allow such violations often force programmers to resort to solutions that are worse than the disease. What is going on here? We want to find out. Here are some preliminary thoughts.

A method for adding IFC to existing programming languages

Information-flow control is a promising discipline for enforcing the security of systems. Unfortunately, adding IFC often requires invasive changes to the semantics of the host language. We're working on a general method for adding coarse-grained IFC to a language, while requiring only minimal changes to our semantics. Inspired by Matthews' and Findler's work on multi-language semantics, our approach is to take a minimal IFC calculus and combine it with the target language to achieve an IFC-enabled language. We hope to validate this approach by showing that the noninterference proof is parametric in the source of language, and that the resulting semantics accurately describe existing IFC systems. Here is a preprint on the topic.

The runtime system of a lazy, purely functional language

GHC's runtime system is a complicated beast, its many lines of code spanning many different concerns. How does parallelism and concurrency work? How does the garbage collector work? How is lazy evaluation implemented? These are questions whose answers are scattered throughout the various literature that has come out of the GHC project over the years. We're working on a journal paper which ties all of this literature together, with the hopes that it will be useful for other designers of runtime systems for functional languages (and perhaps non-functional ones too). Here is a draft version of the paper.

Recent publications

What do I do in my free time?

Some projects I'm associated with...

Metro Maps
of the News
a visual metaphor for interconnected story lines
(joint work with Dafna Shahaf, Russell Chou and Jacob Jensen)
hp/D3.js an interactive GHC heap profile pastebin
Logitext an interactive textbook for teaching the sequent calculus
GHC a compiler for the functional language Haskell
HTML Purifier a standards compliant HTML filter
Wizard a distributed autoinstall management system
CSRF Magic automatic protection against Cross-Site Request Forgery
Monad.Reader a magazine about all things Haskell
(I’m editor: send me a note if you want to write something!)