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.

Verified Scheduling

We present a Coq framework for optimizing high-performance tensor programs via verified, algebraic rewrites. Paper 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