About
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 for ISLE, a term-rewriting language for instruction lowering within Cranelift (a native code generator for WebAssembly 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.
News
- Our verifier for Cranelift’s instruction selection won a Distinguished Artifact Award for ASPLOS 2024! [November 2023]
- 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. [May 2023]
- I served on the program committees of the EGRAPHS workshop and the Student Research Competition at PLDI. [April 2023]
- I presented our work on verifying Cranelift’s Wasm-to-Native instruction selection at the Foundations of WebAssembly Dagstuhl seminar.
- 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 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]
Publications
Conference Papers
-
“Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection”. Alexa VanHattum, Monica Pardeshi, Chris Fallin, Adrian Sampson, Fraser Brown. To appear at ASPLOS 2024. (Preprint local pdf).
-
“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)
Short Papers
- “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).
Dissertation
- “Lightweight Formal Methods for Correct, Efficient Systems Programming”. PhD Dissertation, Cornell University, August 2023.
Recorded Talks
- 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]
Teaching
Wellesley College
- CS340: Modeling for Computer Systems [Spring 2024]
- CS240: Foundations of Computer Systems [Spring 2024, Fall 2023]
Cornell University
- 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]
Brown University
- 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]
Service
- I am on the program committee for the Workshop on Principles of Secure Compilation at POPL.
- I am on the program committee for the Programming Languages and Analysis for Security at POPL.
- I am a co-organizer for PLMW@PLDI 2024.
- 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 Student Research Competition at MICRO.
- 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.