Deciding kCFA is complete for EXPTIME (with D. Van Horn). 2008 ACM International Conference on Functional Programming.
Flow analysis, linearity, and PTIME (with D. Van Horn). 2008 ACM Static Analysis Symposium. Relating complexity and precision in control flow analysis (with D. Van Horn). 2007 ACM International Conference on Functional Programming.
On the complexity of cut elimination in linear logic. (with K. Terui). 2003 Italian Conference on Theoretical Computer Science , LNCS 2841, pp. 23-36.
Constraint semantics, monads, and graph reduction (with A. Bawden).
From Hilbert spaces to Dilbert spaces: context semantics made simple. FSTTCS Kanpur, India, 2003 LNCS 2556:2--17.
LAL is square: representation and expressiveness in light affine logic (with P.M. Neergaard). 2002 Workshop on Implicit Computational Complexity, Copenhagen.
Types, potency, and idempotency: why nonlinearity and amnesia make a type system work (with P.M. Neergaard). 2004 International Conference on Functional Programming , pp. 138-149.
How light is safe recursion? Translations between logics of polynomial time (with P.M. Neergaard).
Linear lambda calculus and PTIME-completeness. J. Functional Programming 14:623-633.
Proofnets and context semantics for the additives (with X. Rival). 2002 Conference on Computer Science Logic, LNCS 2471, pp. 151-166.
Sharing continuations: proofnets for languages with explicit control. (with J. L. Lawall) 2000 European Symposium on Programming (ESOP), pp. 245--259.
Relating typability and expressiveness in finite-rank intersection type systems (with A.J. Kfoury, F. Turbak, and J. Wells). 1999 ACM International Conference on Functional Programming, pp. 90--101.
Parallel beta reduction is not elementary recursive. (with A. Asperti). 1998 ACM Symposium on the Principles of Programming Languages, pp. 303--315. To appear in Information and Computation.
On the global dynamics of optimal graph reduction (with J. L. Lawall). 1997 ACM International Conference on Functional Programming.
Optimality and inefficiency: what isn't a cost model of the lambda calculus? (with J. L. Lawall). 1996 ACM International Conference on Functional Programming, pp. 92--101.
Database query languages embedded in the typed lambda calculus (with G. Hillebrand and P. C. Kanellakis). Information and Computation 127:2 (June, 1996), pp. 117-144. (An extended abstract appeared in the proceedings of the 1993 IEEE Symposium on Logic in Computer Science, pp. 332-343.)
Undecidable boundedness problems for datalog programs (with G. G. Hillebrand, P. C. Kanellakis, and M. Y. Vardi) Journal of Logic Programming 25:2 (1995), pp. 163-190. (An extended abstract appeared in the proceedings of the 1991 ACM Symposium on the Principles of Database Systems, pp. 1-13.)
The complexity of type inference for higher-order typed lambda calculi (with F. Henglein). Journal of Functional Programming 4:4 (1994), pp. 435-478.
An analysis of the Core-ML language: expressive power and type reconstruction (with G. Hillebrand and P. C. Kanellakis). 1994 International Colloquium on Automata, Languages, and Programming (ICALP). Lecture Notes in Computer Science, vol. 820, pp. 83-106.
A constructive logic of multiple subtyping. 1993 ACM Symposium on the Principles of Programming Languages, pp. 313-324.
Quantifier elimination and parametric polymorphism in programming languages. Journal of Functional Programming 2:2 (1992), pp. 213-226.
A simple proof of a theorem of Statman Theoretical Computer Science 103 (1992), pp. 387-394.
Unification and ML type reconstruction (with P. C. Kanellakis and J. C. Mitchell). Computational Logic: Essays in Honor of Alan Robinson (ed. J.-L. Lassez and G. D. Plotkin), pp. 444-478. MIT Press, 1991.
Outline of a proof theory of parametricity. 1991 ACM Symposium on Functional Programming and Computer Architecture. Lecture Notes in Computer Science, vol. 523, pp. 313-327.