mairson

257 Volen / (781) 736-2724

*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.

This material is based upon work supported by the National Science Foundation under Grants 9216185 (Logic, Complexity and Programming Languages), 9619638 (Programming Language Foundations of Computation Theory), 9806718 (Design and Analysis of Symmetric, Hybrid Procedure-calling Protocols), and 0228951 (Logic, Linear Naming, and Programming Language Design).

Go back up.

Mail comments to