We present a Coq framework for optimizing high-performance tensor programs via verified, algebraic rewrites. Paper available.
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.
Rippl is a toy language with a range of Haskell-inspired features including partial application, type inference, lazy semantics, and list comprehensions.
Optimization Via High-Level
Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, Jonathan Ragan-Kelley
Proceedings of the 49th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022)