### Static cost analysis

- Recurrence extraction for functional programs through call-by-push-value (with G. A. Kavvos, Edward Morehouse, and Daniel R. Licata). To appear in
*Proceedings of the ACM on Programming Languages (POPL), 2020*. DOI: 10.1145/3371083. - The main way of analyzing the complexity of a program is that of extracting and solving a recurrence that expresses its running time in terms of the size of its input. We develop a method that automatically extracts such recurrences from the syntax of higher-order recursive functional programs. The resulting recurrences, which are programs in a call-by-name language with recursion, explicitly compute the running time in terms of the size of the input. In order to achieve this in a uniform way that covers both call-by-name and call-by-value evaluation strategies, we use Call-by-Push-Value (CBPV) as an intermediate language. Finally, we use domain theory to develop a denotational cost semantics for the resulting recurrences.
Availability: arXiv.

- Denotational cost semantics for functional languages with inductive types (with D. Licata and R. Ramyaa). In Fisher, K. and Reppy, J. (eds.),
*Proceedings of the 20th ACM SIGPLAN I**nternational Conference on Functional Programming (ICFP 2015)*, pp. 140-151, 2015. DOI: 10.1145/2784731.2784749. - A central method for analyzing the asymptotic complexity of a functional program is to extract and then solve a recurrence that expresses evaluation cost in terms of input size. The relevant notion of input size is often specific to a datatype, with measures including the length of a list, the maximum element in a list, and the height of a tree. In this work, we give a formal account of the extraction of cost and size recurrences from higher-order functional programs over inductive datatypes. Our approach allows a wide range of programmer-specified notions of size, and ensures that the extracted recurrences correctly predict evaluation cost. To extract a recurrence from a program, we first make costs explicit by applying a monadic translation from the source language to a complexity language, and then abstract datatype values as sizes. Size abstraction can be done semantically, working in models of the complexity language, or syntactically, by adding rules to a preorder judgement. We give several different models of the complexity language, which support different notions of size. Additionally, we prove by a logical relations argument that recurrences extracted by this process are upper bounds for evaluation cost; the proof is entirely syntactic and therefore applies to all of the models we consider.
Availability: ICFP 2015 proceedings – arXiv.

- A static cost analysis for a higher-order language (with J. Paykin and J.S. Royer). In Might, M. and Van Horn, D. (eds.),
*Proceedings of the 7th Workshop on Programming Languages Meets Program Verification*, pages 25-34. ACM Press, 2013. - We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a potential. The former is defined to be the size of the expression’s evaluation derivation in a standard big-step operational semantics. The latter is a measure of the “future” cost of using the value of that expression. A translation function maps target expressions to complexities. Our main result is the following Soundness Theorem: If is a term in the target language, then the cost component of is an upper bound on the cost of evaluating . The proof of the Soundness Theorem is formalized in Coq, providing certified upper bounds on the cost of any expression in the target language.
Availability: PLPV 2013 proceedings – arXiv.

### Implicit computational complexity

- Two algorithms in search of a type system (with J. Royer).
*Theory of Computing Systems*45(4):787-821, 2009. This is the full version of our CIE’07 paper. - The authors’ programming formalism is a version of call-by-value under a complexity-theoretically motivated type system. programs run in type- polynomial-time and all standard type basic feasible functionals are -definable ( types are confined to levels , , and~ ). A limitation of the original version of is that the only directly expressible recursions are tail-recursions. Here we extend so that a broad range of affine recursions are directly expressible. In particular, the revised can fairly naturally express the classic insertion- and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based formalisms. The paper’s main work is in refining the original time-complexity semantics for to show that these new recursion schemes do not lead out of the realm of feasibility.
Availability:

*Theory of Computing Systems*– arXiv. - Time-complexity semantics for feasible affine recursions (with J. Royer). In Cooper, S.B., Lowe, B.L., and Sorbi, A. (eds.),
*Computation in the Real World (Proceedings of Computability in Europe 2007, Siena)*, vol. 4497 of*Lecture Notes in Computer Science*, Springer-Verlag, Berlin, 2007. This is the conference version of our Theory of Computing Systems paper. - The authors’ programming formalism is a version of call-by-value under a complexity-theoretically motivated type system. programs characterize the type-level basic feasible functions (-types are confined to levels , , and ). A limitation of the original version of is that the only directly expressible recursions are tail-recursions. Here we extend so that a broad range of affine recursions are directly expressible. In particular, the revised can fairly naturally express the classic insertion- and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based formalisms. The paper’s main work is in extending and simplifying the original time-complexity semantics for to develop a set of tools for extracting and solving the higher-type recurrences arising from feasible affine recursions.
Availability:

*CIE 2007*proceedings – arXiv (extended version). - Adventures in time and space (with J. Royer).
*Logical Methods in Computer Science*3(1):1-53, 2007. This is the full veresion of our POPL ’06 paper. - This paper investigates what is essentially a call-by-value version of under a complexity-theoretically motivated type system. The programming formalism, , has its first-order programs characterize the polynomial-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The -types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook’s and Leivant’s implicit characterizations of polynomial-time. The time-restricting part is an affine version of Barber and Plotkin’s DILL. Two semantics are constructed for . The first is a pruning of the naive denotational semantics for . This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ‘s time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is also shown to be sound relative to the costs of interpretation on the abstract machine.
Availability: Logical Methods in Computer Science.

- Adventures in time and space (with J. Royer). In Jones, S.P. (ed.),
*33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006)*, pp. 168-179, 2006. This is the conference version of our LMCS 2007 paper. - This paper investigates what is essentially a call-by-value version of $\PCF$ under a complexity-theoretically motivated type system. The programming formalism, , has its first-order programs characterize the poly-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The -types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook’s and Leivant’s implicit characterizations of poly-time. The time-restricting part is an affine version of Barber and Plotkin’s DILL. Two semantics are constructed for . The first is a pruning of the naive denotational semantics for . This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ‘s time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is also shown to be sound relative to the costs of interpretation on the abstract machine.
Availability: POPL 2006.

- Minimization and multifunctions (with C. Pollett).
*Theoretical Computer Science*318(1-2):105-119, 2004. - The implicit characterizations of the polynomial-time computable functions given by Bellantoni-Cook and Leivant suggest that this class is the complexity-theoretic analog of the primitive recursive functions. Hence it is natural to add minimization operators to these characterizations and investigate the resulting class of partial functions as a candidate for the analog of the partial recursive functions. We do so in this paper for Cobham’s definition of by bounded recursion and for Bellantoni-Cook’s safe recursion and prove that the resulting classes capture exactly , the nondeterministic polynomial-time computable partial multifunctions. We also consider the relationship between our schemes and a notion of nondeterministic recursion defined by Leivant and show that the latter characterizes the total functions of . We view these results as giving evidence that is the appropriate analog of partial recursive. This view is reinforced by earlier results of Spreen and Stahl who show that for many of the relationships between partial recursive functions and r.e. sets, analogous relationships hold between and sets. Furthermore, since is obtained from in the same way as the recursive functions are obtained from the primitive recursive functions (when defined via function schemes), this also gives further evidence that is properly seen as playing the role of primitive recursion.
- Ramified recurrence with dependent types. In Abramsky, S. (ed.),
*Typed -Calculi and Applications (TLCA 2001)*, vol. 2044 of*Lecture Notes in Computer Science*, Springer-Verlag, Berlin, pp. 91-105, 2001. - We present a version of Godel’s system in which the types are ramified in the style of Leivant and a system of dependent typing is introduced. The dependent typing allows the definition of recursively defined types, where the recursion is controlled by ramification; these recursively defined types in turn allow the definition of functions by repeated iteration. We then analyze a subsystem of the full system and show that it defines exactly the primitive recursive functions. This result supports the view that when data use is regulated (for example, by ramification), standard function constructions are intimately connected with standard type-theoretic constructions.

### Anonymity

- Effectiveness and detection of denial-of-service attacks in Tor (with S. DeFabbia-Kane, D. Krizanc, and M. Liberatore).
*Transactions on Information Systems Security*15(3):11:1-11:25, 2012. - Tor is one of the more popular systems for anonymizing near real-time communications on the Internet. Borisov et al. proposed a denial of service based attack on Tor (and related systems) that significantly increases the probability of compromising the anonymity provided. In this paper, we analyze the effectiveness of the attack using both an analytic model and simulation. We also describe two algorithms for detecting such attacks, one deterministic and proved correct, the other probabilistic and verified in simulation.
Availability:

*Transactions on Information Systems Security*– arXiv.