I am an Assistant Professor of Computer Science at Wellesley College.
My research interests span programming languages and systems, with a focus on applying lightweight formal methods to the compiler stack. I like systems that make it easier for developers to trust their low-level code. Recently, I have been contributing to verification efforts for ISLE, a term-rewriting language for instruction lowering within Cranelift (a native code generator for Wasmtime and an alternative backend for Rust). Previously, I worked on Diospyros, a compiler that uses equality saturation to find vectorization for energy-efficient hardware, and the Kani Rust Verifier, a bit-precise verifier for sequential Rust code.
If you are a Wellesley student interested in research opportunities, please email me or drop by Science Center W116.
I received my PhD from the Department of Computer Science at Cornell University, where I worked in Adrian Sampson’s Computer Architecture and Programming Abstractions research group. I completed my bachelor’s at Brown, where I contributed to projects using modeling tools and refinement types. I spent some time at Apple engineering health software for the iPhone and Apple Watch.
- Our paper on verifying Cranelift’s instruction selection was conditionally accepted at ASPLOS 2024! [August 2023]
- I began as an Assistant Professor of Computer Science at Wellesley. [July 2023]
- I successfully defended my PhD thesis, Lightweight Formal Methods for Correct, Efficient Systems Programming. Written dissertation link to come! [May 2023]
- I served on the program committees of the EGRAPHS workshop and the [Student Research Competition][src23] at PLDI. [April 2023]
- I presented our work on verifying Cranelift’s Wasm-to-Native instruction selection at the Foundations of WebAssembly Dagstuhl seminar.
- I taught CS2110: Object-Oriented Programming and Data Structures this summer. [April 2022]
- I served on the program committee of the EGRAPHS workshop. [March 2022]
- Our paper on verifying dynamic trait objects in Rust was accepted to ICSE SEIP! [January 2022]
- I gave a guest lecture on Diospyros to Wellesley’s Principals of Programming course. [December 2021]
- I passed my A exam (admission to candidacy/thesis proposal)! [December 2021]
- I interned with the AWS Automated Reasoning Group, working on improving dynamic dispatch support within the Kani Rust Verifier. [June 2021]
- I had a blast presenting our work on Diospyros at UCSC’s Languages, Systems, and Data seminar. [December 2020]
- Our full-length paper on Diospyros was accepted to ASPLOS 2021! [November 2020]
- I presented our work-in-progress short paper on Diospyros at LCTES 2020. [June 2020]
- Rachit Nigam and I are finalists for Qualcomm’s Innovation Fellowship. [April 2020]
- I was fortunate to be awarded the NSF’s GRFP fellowship. [March 2020]
- Honored to have my work as a Head TA mentioned in the acknowledgments of Professor Andy van Dam’s Reflections on an introductory CS course, CS15, at Brown University in ACM Inroads. [November 2018]
- “Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection”. (Preprint local pdf). Conditionally accepted to ASPLOS 2024.
“Verifying Dynamic Trait Objects in Rust” Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Sampson. In ICSE Software Engineering in Practice 2022. (local pdf, 20 minute talk video).
“Vectorization for Digital Signal Processors via Equality Saturation” Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, Adrian Sampson. In ASPLOS 2021. (local pdf, 5 minute talk video, 17 minute talk video)
- “A Synthesis-aided Compiler for DSP Architectures (WiP Paper).” Alexa VanHattum*, Rachit Nigam*, Vincent T. Lee, James Bornholt, Adrian Sampson (*equal contribution). In LCTES 2020. (local pdf, talk video).
- Vectorization for Digital Signal Processors via Equality Saturation. ASPLOS 2021. 5 minute talk video, 17 minute talk video.
- A Synthesis-aided Compiler for DSP Architectures (WiP Paper) for LCTES 2020 [June 2020]
- What’s New in Health (slides) at Apple’s World Wide Developers Conference [Spring 2017]
- CS240: Foundations of Computer Systems [Fall 2023]
- Instructor for CS2110: Object-Oriented Programming and Data Structures [Summer 2022]
- Grad TA (part-time) for CS 4110: Programming Languages & Logics [Fall 2020]
- Grad TA for CS 4110: Programming Languages & Logics [Fall 2018]
- Head TA for CS 195y: Logic for Systems [Spring 2016]
- Head TA for CS 15: Intro. Object-Oriented Programming & Computer Science [Fall 2015]
- TA for CS 22: Discrete Math & Probability [Spring 2015]
- TA for CS 15: Intro. Object-Oriented Programming & Computer Science [Fall 2014]
- TA for CS 8: First Byte of Computer Science [Spring 2014]
- I am a co-organizer for PLMW@PLDI 2024.
- I am on the program committee for the 2023 Student Research Competition at MICRO.
- I am on the volunteer committee for SIGPLAN-M, a long-term mentoring program for the programming languages community.
- I was on the program committee for the 2023 EGRAPHS workshop at PLDI.
- I was a judge for the 2023 Student Research Competition at PLDI.
- I co-founded and was on the board for Cornell Graduate Students for Gender Inclusion in Computing from 2019-2023.
- I was on the program committee for the 2022 EGRAPHS workshop at PLDI.
- I co-organized Cornell’s Programming Languages Discussion Group (PLDG) from 2020-2021.
- I was on the OOPSLA 2020 Artifact Evaluation Committee.
- I was on the CS department’s 2020 Fall Teaching Committee.
- I helped organize the CS department’s colloquium talks.
- I co-organized Cornell’s 2019 Admitted PhD Student Visit Day.