Programming languages and privacy
Static cost analysis
My work on this area focuses on the extraction of cost recurrences from programs, most recently focusing on functional languages with support for a wide variety of inductive datatypes with user-defined notions of size. The goal is not to “build a better mousetrap”—i.e., develop recurrence extraction techniques that apply to programs that cannot be analyzed by other means. Rather, the point is to use denotational semantics to justify the “everyday reasoning” we typically teach and use to analyze algorithms
- Denotational semantics as a foundation for recurrence extraction for functional languages (JFP 2022)
- Denotational recurrence extracction for amortized analysis (ICFP 2020)
- Recurrence extraction for functional languages through call-by-push-value (POPL 2020)
Implicit computational complexity (ICC)
ICC is the study of language-based techniques for restricting the resource use of programs, often through type-theoretic means. On the one hand, I am interested in the development of “usable” programming languages with guaranteed resource usage based on the theoretical results from ICC. On the other hand, I am also interested in extending the techniques of ramification of safe/normal distinctions to higher-order languages, data with sharing, and coinductively-defined data.