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.
🗣️ Visiting the PL and Graphics groups at Brown University to give a talk.
🗣️ We have a Dagstuhl on EGRAPHS!
🧰 PLDI 2025 was a huge success! Many thanks to everyone who helped me out as Program Chair!!
🗣️ SIGPLAN Research Highlights featured our POPL paper on egg!
🗣️ Gave a talk at Cornell’s CS Colloquium on our work on equality saturation. Many thanks to Nate for hosting!
🗣️ Excited to start this quarter as Full Professor!
🗣️ Offered a week-long seminar at the Marktoberdorf summer school on analysis and optimizations with equality saturation.
🗣️ 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.
🧑🏫 I will be teaching Emina’s course on Solver-aided Programming (CSE 507) this quarter!
🗣️ Edward is presenting Odyssey at FPTalks 2023.
🎯 Pavel and I are co-organizing FPTalks 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.
⛰️ Anjali and I are co-organizing PNW PLSE 2023.
🗣️ David is presenting babble at POPL 2023.
🧑🏫 James and I are co-teaching Grad PL (CSE 505).
Please see past news for more.
Please see my students page for more.
Target-Aware Implementation of Real Expressions
Brett Saiki,
Jackson Brough,
Jonas Regehr,
Jesús Ponce,
Varun Pradeep,
Aditya Akhileshwaran,
Zachary Tatlock,
Pavel Panchekha
Architectural Support for Programming Languages and Operating Systems (ASPLOS) 2025
Application-level Validation of Accelerator Designs Using a Formal Software/Hardware Interface
Bo-Yuan Huang,
Steven Lyubomirsky,
Yi Li,
Mike He,
Gus Henry Smith,
Thierry Tambe,
Akash Gaonkar,
Vishal Canumalla,
Andrew Cheung,
Gu-Yeon Wei,
Aarti Gupta,
Zachary Tatlock,
Sharad Malik
ACM Transactions on Design Automation of Electronic Systems (TODAES) 2024
Computational Illusion Knitting
Amy Zhu,
Yuxuan Mei,
Benjamin Jones,
Zachary Tatlock,
Adriana Schulz
ACM Transactions on Graphics (TOG) 2024
FPGA Technology Mapping Using Sketch-Guided Program Synthesis
Gus Henry Smith,
Benjamin Kushigian,
Vishal Canumalla,
Andrew Cheung,
Steven Lyubomirsky,
Sorawee Porncharoenwase,
René Just,
Gilbert Louis Bernstein,
Zachary Tatlock
Architectural Support for Programming Languages and Operating Systems (ASPLOS) 2024
Magic Markup: Maintaining Document-External Markup with an LLM
Edward Misback,
Zachary Tatlock,
Steven L. Tanimoto
<Programming> 2024
Equality Saturation Theory Exploration à la Carte
Anjali Pal,
Brett Saiki,
Ryan Tjoa,
Cynthia Richey,
Amy Zhu,
Oliver Flatt,
Max Willsey,
Zachary Tatlock,
Chandrakana Nandi
Object-Oriented Programming, Systems, Languages & Applications (OOPSLA) 2023
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.
2025 Autumn, UW CSE 507: Computer-Aided Reasoning for Software
2023 Autumn, UW CSE 507: Computer-Aided Reasoning for Software
Please see my teaching page for more.
My colleague Dan Grossman characterizes this combination of formalism and empiricism as “both Greek and graphs”.↩︎
