Hello! My name is Amanda Liu. Currently, I work on the XLA TPU Compiler at Google. Before that, I completed my PhD at MIT advised by Jonathan Ragan-Kelley and Adam Chlipala. My work focused on developing a formally-verified tensor-program optimization framework and compiler using the Rocq proof assistant. My research interests broadly include formal verification, high-performance systems, compilers, and types! I'm interested in using formal methods and programming languages to develop verified, principled methods for writing high-performance systems.

Verified Scheduling

We present a Rocq framework for optimizing high-performance tensor programs via verified, algebraic rewrites. Thesis available.

Closure JavaScript Bounded Generics

Closure is Google's internal optimizing JavaScript compiler. I implemented bounded generic template types within Closure JavaScript's type system.

Wyvern Architecture Description Lang.

ArchWyvern is an architecture description language implemented on top of Wyvern. It's used to generate secure, scalable software architectures. Extended abstract and presentation available.

Rippl Language

Rippl is a toy language with a range of Haskell-inspired features including partial application, type inference, lazy semantics, and list comprehensions.

• Full CV