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.
|phone||+1 412 268 6309|
|address||Computer Science Department
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213-3891
|Apr 2, 2021||Our articles Central Moment Analysis for Cost Accumulators in Probabilistic Programs and Sound Probabilistic Inference via Guide Types have been accepted to PLDI 2021.|
|Nov 4, 2020||The articles Modeling and Analyzing Evaluation Cost of CUDA Kernels and A unifying type-theory for higher-order (amortized) cost analysis have been accepted to POPL 2021.|
|Oct 25, 2020||We have created a website for Nomos. It’s still work in progress but you can already implement, type-check, and run smart contracts using an interactive web interface.|
|Oct 20, 2020||I’m excited that John Grosen has joined my group as a PhD student. Welcome to Carnegie Mellon, John!|
|Sep 26, 2020||I’m excited that our article Typable Fragments of Polynomial Automatic Amortized Resource Analysis has been accepted to CSL 2021. Congratulations, Long Pham!|
|Jul 10, 2020||Our acricle Resource-Aware Session Types for Digital Contracts has been accepted to CSF’21.|
|Jul 1, 2020||Effective today, I have been promoted to Association Professor without tenure. Many thanks to my colleagues in the Computer Science Department and at Carnegie Mellon.|
|Jun 22, 2020||A new working paper is online: Typable Fragments of Polynomial Automatic Amortized Resource Analysis. This is joined work with my PhD student Long Pham.|