I am an Associate Professor at Carnegie Mellon’s Computer Science Department, and a member of the Principles of Programming (PoP) group and CyLab.

My research areas are programming languages and verification. My mission is to discover beautiful mathematical ideas that have a real-world impact, shape the way programmers think, and help to create software that is more reliable, efficient, and secure. Currently, I am working on quantitative verification, type systems, static resource analysis of programs, probabilistic programming, and programming languages for digital contracts.

Before joining Carnegie Mellon, I was an Associate Research Scientist in the FLINT group at the Department of Computer Science at Yale University. Before that, I was a PhD student at LMU Munich. My advisor was Martin Hofmann.

news

Oct 25, 2026 Our paper Bao: Automatic Region Placement and Memory Allocation for Intermittent Computing (with Byeongjee Kang, Limin Jia, Brandon Lucia, Feras Saad) will appear at ASPLOS ‘27.
Aug 1, 2026 I will serve on the review committees of OOPSLA ‘27 and PLDI ‘27. Consider submitting!
Apr 17, 2026 Our article LFPL: Revisited and Mechanized has been accepted at LICS 2026. Congrats to first author Nathan Glover.
Feb 25, 2026 Our article Handling Exceptions and Effects with Automatic Resource Analysis as been accepted to OOPSLA 2026. Congrats to Ethan Chu on his first first-author paper.
Feb 25, 2026 I’m looking forward to serving on the program committee of Computer Science Logic (CSL) 2027.
Jan 1, 2026 I’m excited to teach and design a new course on probabilistic programming languages together with Feras Saad this spring.
Nov 6, 2025 Our article on Big Stop Semantics as been accepted to POPL 2026. I’m looking forward to seeing in at POPL in Rennes.
Oct 1, 2025 I’m excited that the NSF selected our proposal on FMitF: Track I: Probabilistic Modeling and Analysis Tools for Intermittent Systems for an award. This is a joint project with Limin Jia, Feras Saad, and Brandon Lucia.

Show all news