Education

Ph.D.:

Indiana University, Bloomington, 1999, Mathematics. Thesis title: Ordinal Notations in Typed λ-Calculi. Thesis advisor: Daniel Leivant.

B.A.:

University of California, Berkeley, 1991, Mathematics.

Employment

July 2009– :

Associate Professor of Computer Science, Wesleyan University, Department of Mathematics and Computer Science.

August 2002–June 2009:

Assistant Professor of Computer Science, Wesleyan University, Department of Mathematics and Computer Science.

August 1999–August 2002:

VIGRE Assistant Professor and Adjunct Assistant Professor, University of California, Los Angeles, Mathematics Department (Program in Computing).

Research Interests

My primary research focus is the development of practical programming languages with guaranteed resource usage (e.g., the programs are guaranteed to run in polynomial-time). These guarantees are made by type-theoretic constraints motivated by results of Leivant and Bellantoni and Cook in implicit computational complexity. However, designing a usable higher-order functional language poses a number of very interesting research problems in both practical and foundational areas.

I am also interested in 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.

Refereed Publications

• Detecting denial-of-service attacks in Tor (with D. Krizanc and M. Liberatore). To appear in Financial Cryptography 2009.
• 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.
• Two algorithms in search of a type system (with J. Royer). To appear in Theory of Computing Systems. http://dx.doi.org/10.1007/s00224-009-9181-y.
• Creating an academic community to build humanitarian FOSS: A progress report (with T. de Lanerolle, R. Morelli, et al.). 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.
• Circuit principles and weak pigeonhole variants (with C. Pollett). Theoretical Computer Science 383(2):115–131, 2007. http://dx.doi.org/10.1016/j.tcs.2007.04.017.
• 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), pp. 205–217. Springer-Verlag (Lecture Notes in Computer Science 4497), Berlin, 2007. http://dx.doi.org/10.1007/978-3-540-73001-9_22.
• Adventures in time and space (with J. Royer). Logical Methods in Computer Science 3(1):1–53, 2007. http://arxiv.org/abs/cs/0612116v3.
• The weak pigeonhole principle for function classes in S₂¹ (with C. Pollett). Mathematical Logic Quarterly 52(6):575–584, 2006. http://dx.doi.org/10.1002/malq.200610015.
• 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. http://doi.acm.org/10.1145/1111037.1111053.
• 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.
• Minimization and NP-multifunctions (with C. Pollett). Theoretical Computer Science 318(1–2):105–119, 2004. http://dx.doi.org/10.1016/j.tcs.2003.10.020.
• 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. http://dx.doi.org/10.1007/3-540-45413-6_11.
• Stratified polymorphism and primitive recursion (with D. Leivant). Mathematical Structures in Computer Science 9(4):507–522, 1999. http://dx.doi.org/10.1017/S0960129599002868.
• Ordinals and ordinal functions representable in the simply typed lambda calculus. Annals of Pure and Applied Logic 97(1–3):179–201, 1999. http://dx.doi.org/10.1016/S0168-0072(98)00046-3.
• On the foundations of corecursion (with L. S. Moss). Logic Journal of the IGPL 5(2), 1997. http://dx.doi.org/10.1093/jigpal/5.2.231.
• Towards a model theory of diagrams (with E. Hammer). Journal of Philosophical Logic 25(5):463–482, 1996. Reprinted as “Towards a model theory of Venn diagrams” in G. Allwein and J. Barwise (eds.), Logical Reasoning with Diagrams, pp. 109–127. Oxford University Press (Studies in Logic and Computation 6), New York, 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. thesis, Indiana University, 1999.

Conference Presentations

Technical Symposium on Computer Science Education (SIGCSE) 2008, Portland:

Teaching and building humanitarian open source software (with T. de Lanerolle, R. Morelli, et al.).

Workshop on Implicit Computational Complexity 2008, Villetaneuse:

Affine tiered recursion: semantics and pragmatics.

Computability in Europe 2007, Siena:

Two algorithms in search of a type system.

Typed λ-Calculi and Applications 2001, Kraków:

Ramified recurrence and dependent types.

Association for Symbolic Logic Annual Meeting 1999, San Diego:

Stratified polymorphism and primitive recursion.

Association for Symbolic Logic Annual Meeting 1998, Toronto:

Ordinal notations in typed λ-calculi.

Major Grants Received

National Science Foundation CPATH CB Collaborative Grant:

Can humanitarian open-source development help revitalize undergraduate computing education? (Co-PI with Ozgur Izmirli [Connecticut College], Danny Krizanc [Wesleyan University], Ralph Morelli [Trinity College], Gary Parker [Connecticut College]) The activities funded by this grant center around using open-source software development, with a focus on software for humanitarian and community needs, as a tool for attracting, motivating, and retaining undergraduate students in Computer Science. Fall 2007–Summer 2009. Amount: $496,429.

Mellon Foundation:

Spring 2005. Joint grant application (with Connecticut College and Trinity College) to Mellon Foundation for funding pedagogical and research initiatives for Computer Science departments at small liberal arts institutions. Amount: $800,000.

Professional Activities

Referee:

Annals of Pure and Applied Logic, 2003, 2006; Information and Computation, 2002, 1997; ICALP, 2009; Journal of Functional Programming, 2002; Logic in Computer Science, 1999, 1996. Logic of Programming and Automated Reasoning, 2000; Logical Methods in Computer Science, 2008; Proof Theory and Computer Science, 2001; SIAM Journal on Computing, 2004; TYPES Conference, 2003;

Reviewer:

Mathematical Reviews, 2000–2003; Bulletin of Symbolic Logic, 2001–2002.

Teaching Experience

Wesleyan University, Department of Computer Science:

Undergraduate: Crypotgraphy (first-year seminar); Privacy and security (first-year seminar); Computer Science I; Data Structures; Design and analysis of algorithms; Programming methods/software development; Computer graphics. Graduate: Logic and discrete mathematics; Proof theory; Topics in theoretical computer science.

University of California, Los Angeles, Program in Computing:

Undergraduate: Introduction to computers; C++ programming (first- and second-quarter); Java programming (first- and second-quarter); Computability and complexity theory.

Summer 2001:

Faculty advisor, Research Experiences for Undergraduates, Indiana University, Bloomington, Mathematics Department. Responsible for guiding an undergraduate student in an eight-week research project in programming language theory.

August 1994–May 1999:

Associate Instructor (Graduate Student Instructor), Indiana University, Bloomington, Mathematics Department. Responsible for assisting large lecture courses, as well as teaching College Algebra, Finite Mathematics, Brief Calculus, Mathematics for Elementary Education Majors, and Introduction to Mathematical Problem Solving.