ztatlock
A zebra with sunglasses and laser eyes spelling Z.

Zachary Tatlock

My goal is to help students become great computer scientists. On the research front, I work towards this goal with my students in the PLSE research group. On the education front, I work towards this goal by teaching courses on programming languages and related topics.

My expertise is rooted in formal verification, especially of compilers. As my students develop their own research vision, we branch out across diverse domains. Our work is unified by themes of making it easier to write tricky code and figuring out how to ensure such programs are correct. We rigorously prove our results and always build real, working systems1. Some of the domains we have explored include:

Check out our projects, publications, and talks for more!


  1. My colleague Dan Grossman characterizes this combination of formalism and empiricism as “both Greek and graphs”.  ↩︎