Zachary Tatlock

Associate Professor (photo)
Paul G. Allen School of Computer Science & Engineering
University of Washington

My goal is to help students become great computer scientists. In research, I work toward this goal with my students in the UW PLSE research group. In education, I work toward 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 remains 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 while building and measuring real systems1.


October 2023

🗣️  Anjali is presenting Enumo at OOPSLA 2023.

🗣️  Edward is presenting Odyssey at UIST 2023.

🧰  Released Ian’s Amazon internship project on Haploid, an egg-based SMT query simplifier.

September 2023

🧑‍🏫  I will be teaching Emina’s course on Solver-aided Programming (CSE 507) this quarter!

July 2023

🗣️  Edward is presenting Odyssey at FPTalks 2023.

🎯  Pavel and I are co-organizing FPTalks 2023.

June 2023

🗣️  Yihong is presenting egglog at PLDI 2023.

🗣️  Gus is presenting Lakeroad at PLARCH 2023.

🧰  Max and I are co-organizing EGRAPHS 2023.

🗣️  Oliver is giving the first egglog demo at EGRAPHS 2023.

🗣️  Yihong is giving a talk on tree automata at EGRAPHS 2023.

May 2023

⛰️  Anjali and I are co-organizing PNW PLSE 2023.

January 2023

🗣️  David is presenting babble at POPL 2023.

🧑‍🏫  James and I are co-teaching Grad PL (CSE 505).

Please see past news for more.

Current Students

Please see my students page for more.

Recent Publications

Odyssey: An Interactive Workbench for Expert-Driven Floating-Point Expression Rewriting
Edward Misback,  Caleb C. Chan,  Brett Saiki,  Eunice Jun,  Zachary Tatlock,  Pavel Panchekha
ACM Symposium on User Interface Software and Technology (UIST) 2023

Generate Compilers from Hardware Models!
Gus Henry Smith,  Ben Kushigian,  Vishal Canumalla,  Andrew Cheung,  René Just,  Zachary Tatlock
Workshop on Programming Languages and Computer Architecture (PLARCH) 2023

Better Together: Unifying Datalog and Equality Saturation
Yihong Zhang,  Yisu Remy Wang,  Oliver Flatt,  David Cao,  Philip Zucker,  Eli Rosenthal,  Zachary Tatlock,  Max Willsey
Programming Language Design and Implementation (PLDI) 2023

babble: Learning Better Abstractions with E-Graphs and Anti-Unification
David Cao,  Rose Kunkel,  Chandrakana Nandi,  Max Willsey,  Zachary Tatlock,  Nadia Polikarpova
Principles of Programming Languages (POPL) 2023

Small Proofs from Congruence Closure
Oliver Flatt,  Samuel Coward,  Max Willsey,  Zachary Tatlock,  Pavel Panchekha
Formal Methods in Computer-Aided Design (FMCAD) 2022

Verified Compilation and Optimization of Floating-Point Programs in CakeML
Heiko Becker,  Robert Rabe,  Eva Darulova,  Magnus O. Myreen,  Zachary Tatlock,  Ramana Kumar,  Yong Kiam Tan,  Anthony Fox
European Conference on Object-Oriented Programming (ECOOP) 2022

Co-Optimization of Design and Fabrication Plans for Carpentry
Haisen Zhao,  Max Willsey,  Amy Zhu,  Chandrakana Nandi,  Zachary Tatlock,  Justin Solomon,  Adriana Schulz
ACM Transactions on Graphics (TOG) 2022

Relational e-matching
Yihong Zhang,  Yisu Remy Wang,  Max Willsey,  Zachary Tatlock
Principles of Programming Languages (POPL) 2022

Please see my publications page for more.

Recent Teaching

Please see my teaching page for more.

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