Wesleyan University
Department of Mathematics and Computer Science
265 Church St., Science Tower 655
Middletown, CT 06549-0128
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:
- 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:
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:
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: