Office: Science Tower 629
Static cost analysis
My primary research interest is the development of formal tools for reasoning about complexity of higher-order languages. One aspect of this is the extraction of cost information for higher-order programs from source code. My current work on this area focuses on the extraction of recurrences from programs, most recently focusing on functional languages with support for a wide variety of inductive datatypes with user-defined notions of size. A long-term goal is the development of a system that permits the extraction of recurrences into a proof assistant environment, wherein the user can reason about those recurrences in order to ultimately provide certified bounds on the execution cost of the source program.
- Denotational semantics as a foundation for recurrence extraction for functional languages (JFP 2022).
- Denotational recurrence extraction for amortized analysis (ICFP 2020).
- Recurrence extraction for functional programs through call-by-push-value (POPL 2020).
- Denotational cost semantics for functional languages with inductive types (ICFP 2015).
- A static cost analysis for a higher-order language (PLPV 2013).
Implicit computational complexity
Another aspect of reasoning about higher-order complexity is the application of techniques from implicit computational complexity. 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.
- General ramified recurrence and polynomial-time completeness.
- Two algorithms in search of a type system.
- Adventures in time and space.
My other research focus is privacy issues in general and anonymizing systems in particular. Many published attacks on such systems have been investigated primarily by simulation or by a mathematical analysis based on assumptions about traffic through such systems. I am interested in the practical effects and impacts of such attacks. I am currently starting a research program to investigate the possibilities of simulating network behavior by using machine-learning techniques. I am also interested in simulation methodologies in general, and how to quantify the quality of a simulation (e.g., of an anonymity network) in particular.