The documents referenced below are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author’s copyright.

Refereed publications

Implicit computational complexity and resource-bounded languages.

Two algorithms in search of a type system (with J. Royer). To appear in Theory of Computing Systems. This is the full version of our CIE’07 paper Time-complexity semantics for feasible affine recursions.

Abstract: The authors’ ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR-definable (ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR 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 ATR to show that these new recursion schemes do not lead out of the realm of feasibility.

Availability: Journal—arXiv.

Time-complexity semantics for feasible affine recursions (with J. Royer). In S.B. Cooper, B. Löwe, and A. Sorbi (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 “Two algorithms in search of a type system.”

Abstract: The authors’ ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs characterize the type-level < 2 basic feasible functions (ATR-types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR 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 ATR to develop a set of tools for extracting and solving the higher-type recurrences arising from feasible affine recursions.

Availability: Proceedings—arXiv. For the journal version, see our Theory of Computing Systems paper “Two algorithms in search of a type system.”

Adventures in time and space (with J. Royer). Logical Methods in Computer Science 3(1):1–53, 2007. This is the full version of our POPL’06 paper of the same name.

Abstract: This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR, 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 ATR-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 ATR. The first is a pruning of the naïve denotational semantics for ATR. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR’s time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATRrecursions, 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: Journal.

Adventures in time and space (with J. Royer). In Jones, S. P. (ed.), Annual Symposium on Principles of Programming Languages (Charleston, SC, 2006), pp. 168–179. Association for Computing Machinery, New York, 2006. This is the conference version of our Logical Methods in Computer Science paper of the same name.

Abstract: This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR₁, 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 ATR₁-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 ATR₁. The first is a pruning of the naïve denotational semantics for ATR₁. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR₁’s time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATR₁ 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: Proceedings. For the journal version see our Logical Methods in Computer Science paper of the same name.

Minimization and NP multifunctions (with C. Pollett). Theoretical Computer Science 318(1–2):105–119, 2004.

Abstract: The implicit characterizations of the polynomial-time computable functions FP 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 FP by bounded recursion and for Bellantoni-Cook’s safe recursion and prove that the resulting classes capture exactly NPMV, 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 NPMV. We view these results as giving evidence that NPMV 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 NPMV and NP sets. Furthermore, since NPMV is obtained from FP 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 FP is properly seen as playing the role of primitive recursion.

Availability: Journal.

Ramified recurrence with dependent types. In S. Abramsky (ed.), Typed -Calculi and Applications (Kraków 2001), pp. 91–105. Springer-Verlag (Lecture Notes in Computer Science 2044), Berlin, 2001.

Abstract: We present a version of Gödel’s system T 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.

Availability: Proceedings.

Stratified polymorphism and primitive recursion (with D. Leivant). Mathematical Structures in Computer Science 9(4):507–522, 1999.

Abstract: Natural restrictions on the syntax of the second order (i.e. polymorphic) lambda calculus are of interest for programming language theory. In [D. Leivant, Finitely stratified polymorphism, Information and Computation, 93(1):93–114, 1991] one of the authors showed that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level ₄in the Grzegorczyk Hierarchy). We define here a second order lambda calculus in which type abstraction is stratified to levels up to , an ordinal that permits highly uniform (and finite) type inference rules. Referring to this system, we show that the numeric functions definable in the calculus using ranks < are precisely Grzegorczyk’s class ₊₃ (> 1. This generalizes [D. Leivant, Finitely stratified polymorphism, Information and Computation, 93(1):93–114, 1991], where this is proved for = 1. Thus, the numeric functions definable in our calculus are precisely the primitive recursive functions.

Availability: Journal.

Anonymity.

Detecting denial-of-service attacks in Tor (with D. Krizanc and M. Liberatore). To appear in Financial Cryptography 2009.

Abstract: Tor is currently one of the more popular systems for anonymizing near real-time communications on the Internet. Recently, 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 propose an algorithm for detecting such attacks and examine the effectiveness of the obvious approach to evading such detection. We implement a simplified version of the detection algorithm and study whether the attack may be in progress on the current Tor network. Our preliminary measurements indicate that the attack was probably not implemented during the period we observed the network.

Availability: Not available yet.

Bounded arithmetic and pigeonhole principles.

Circuit principles and weak pigeonhole variants (with C. Pollett). Theoretical Computer Science 383(2):115-131, 2007. This is an improved version of our CATS’05 paper of the same name.

Abstract: This paper considers the relational versions of the surjective, partial surjective, and multifunction weak pigeonhole principles for PV, ₁^b, ₁^b, and B₁^b-formulas as well as relativizations of these formulas to higher levels of the bounded arithmetic hierarchy. We show that the partial surjective weak pigeonhole principle for ₁^b formulas implies that for each k there is a string of length 2^2nk which is hard to block-recognize by circuits of size n^k. These principles in turn imply the partial surjective principle for ₁^b formulas. We show that the surjective weak pigeonhole principle for B₁^b formulas in S₂¹ implies our hard-string principle which in turn implies the surjective weak pigeonhole principle for ₁^b formulas. We introduce a class of predicates corresponding to poly-log length iterates of polynomial-time computable predicates and show that over S₂¹, the multifunction weak pigeonhole principle for such predicates is equivalent to an “iterative” circuit block-recognition principle. A consequence of this is that if S₂¹ proves this principle then RSA is vulnerable to polynomial time attacks.

Availability: Journal—offprint.

The weak pigeonhole principle for function classes in S₂¹ (with C. Pollett). Mathematical Logic Quarterly 52(6):575–584, 2006.

Abstract: It is well known that S₂¹ cannot prove the injective weak pigeonhole principle for polynomial time functions unless RSA is insecure. In this note we investigate the provability of the surjective (dual) weak pigeonhole principle in S₂¹ for provably weaker function classes.

Availability: Journal—preprint.

Circuit Principles and Weak Pigeonhole Variants (with C. Pollett). In M. Atkinson and F. Dehne (eds.), Computing: The Australasian Theory Symposium (Newcastle, Australia, 2005), pp. 31–40. Australian Computer Society (Conferences in Research and Practice in Information Technology 41), Sydney, 2005. This is the conference version of our Theoretical Computer Science paper of the same name.

Abstract: This paper considers the relational versions of the surjective and multifunction weak pigeonhole principles for PV, ₁^b and ₂^b-formulas. We show that the relational surjective pigeonhole principle for ₂^b formulas in S₂¹ implies a circuit block-recognition principle which in turn implies the surjective weak pigeonhole principle for ₁^b formulas. We introduce a class of predicates corresponding to poly-log length iterates of polynomial-time computable predicates and show that over R₂², the multifunction pigeonhole principle for such predicates is equivalent to an “iterative” circuit block-recognition principle. A consequence of this is that if R₃² proves this circuit iteration principle then RSA is vulnerable to quasi-polynomial time attacks.

Availability: For the journal version see our Theoretical Computer Science paper of the same name.

Open-source software in the curriculum.

Revitalizing computing education by building free and open source software for humanity (with R. Morelli, A. Tucker, et al.). To appear in Communications of the ACM.

Abstract: The Humanitarian Free and Open Source Software Initiative (the “HFOSS initiative”) aims to help revitalize undergraduate computing education by engaging students in developing open source software that benefits humanity. Inspired by the Sahana project, a free and open source disaster management system that started in the aftermath of the 2004 Asian tsunami, this initiative includes students from several colleges and universities in a variety of software development projects, both global and local. This paper provides an overview of the HFOSS initiative following its first year of activity. Our experiences suggest that engaging students in building free and open source software that serves society can help invigorate undergraduate computing education.

Availability: Not available yet.

Creating an academic community to build humanitarian FOSS: A progress report. In F. Fiedrich and B. Van de Walle (eds.) Proceedings of the 5th International Conference on Information Systems for Crisis Response and Management (ISCRAM 2008, Washington, D.C.), pp. 337–341.

Abstract: This paper describes The Humanitarian FOSS Project, a National Science Foundation funded effort to help revitalize undergraduate computing education by getting students and faculty involved in building open source software that benefits the community.

Availability: Proceedings.

Other papers.

Ordinals and ordinal functions representable in the simply typed lambda-calculus. Annals of Pure and Applied Logic 97(1–3):179–201, 1999.

Abstract: We define ordinal representations in the simply typed lambda calculus, and consider the ordinal functions representable with respect to these notations. The results of this paper have the same flavor as those of Schwichtenberg and Statman on numeric functions representable in the simply typed lambda calculus. We define four families of ordinal notations; in order of increasing generality of the type of notation, the representable functions consist of the closure under composition of (1) successor and , (2) addition and , (3) addition and multiplication, and (4) addition, multiplication, and a “weak” discriminator.

Availability: Journal.

On the foundations of corecursion (with L. Moss). Logic Journal of the IGPL 5(2):231–257, 1997.

Abstract: We consider foundational questions related to the definition of functions by corecursion. This method is especially suited to functions into the greatest fixed point of some monotone operator, and it is most applicable in the context of non-wellfounded sets. We review the work on the Special Final Coalgebra Theorem of Aczel and the Corecursion Theorem of Barwise and Moss. We offer a condition weaker than Aczel’s condition of uniformity on maps, and then we prove a result relating the operators satisfying the new condition to the smooth operators of Barwise and Moss.

Availability: Journal.

Toward a model theory of diagrams (with E. Hammer). Journal of Philosophical Logic 25(5), 1996.

Other publications

Book review of Derivation and Computation: Taking the Curry-Howard Correspondence Seriously (by H. Simmons). Bulletin of Symbolic Logic 7(3):380–383, 2001.

Ordinal Notations in Typed -Calculi. Ph.D. dissertation, Indiana University, 1999.

Abstract: In this thesis, we investigate the use of various typed -calculi as a basis for ordinal notations. Traditionally, an ordinal notation is constructed as a numeric code, an approach that obscures intuitive notions of complexity. By extending the Church numerals of the -calculus to transfinite ordinal notations, we are able to meet two complexity-theoretic criteria: (1) passing to a limit in the construction of an ordinal (the “complex” step) is made explicit, and (2) there are natural syntactic requirements that restrict the complexity of the possible notations (and hence the ordinals for which there are notations). We carry out this program for the simply typed -calculus and the transfinitely ramified polymorphic -calculus. For the simply typed calculus, we introduce several classes of notations and characterize both the ordinals and ordinal functions representable with respect to each class. For the ramified -calculus, we calibrate the representable ordinals against the degree of ramification. We also define environment model semantics for transfinitely ramified polymorphism and prove that the semantics is sound and complete for -conversion, and investigate iteration functionals in the type structure over the ordinals.