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 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.

My CV.

News

• 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]

Publications

To Appear

• “Lightweight, Modular Verification for WebAssembly-to-Native Instruction Selection”. (Preprint local pdf). Conditionally accepted to ASPLOS 2024.

Conference Papers

• “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).

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

• CS240: Foundations of Computer Systems [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 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.