Research

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.

Related papers:

• Denotational semantics as a foundation for recurrence extraction for functional languages (manuscript).
• 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).

Related code:

• Recurrence extraction tool implementation.

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.

Related papers:

• Two algorithms in search of a type system.
• Adventures in time and space.

Anonymity

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.

Related papers:

• Effectiveness and detection of denial-of-service attacks in Tor.