About Me

Hello! My name's Amanda Liu. I'm a third year PhD student at MIT advised by Jonathan Ragan-Kelley and Adam Chlipala. 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.

Previously, I was an undergraduate at Columbia University and conducted research under Stephen Edwards and Ronghui Gu on programming languages and formal methods for building hardware and secure smart contract languages, respectively.


Two images of a parrot one sharp and one blurred on the left and right with rectangular layers representing an image processing pipeline in between

Verified Scheduling

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

Closure compiler logo

Closure JavaScript Bounded Generics

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

Graphic blue droplet of water

Rippl Language

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


Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, Jonathan Ragan-Kelley
Proceedings of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022)