New Results on Local Inference Relations with Robert Givan, KR, 1992.

Walther Recursion, Conference on Automated Deduction (CADE), 1993.

Automatic Recognition of Tractability in Inference Relations JACM, 1993.

A Proof of Strong Nornalization for F2, Fomega and Beyond with Jakov Kucan and Daniel Otth, Information and Computation, 1995.

Inferring Recursive Data Types. A 1996 paper that was rejected a couple times but remained on my web page. Material form this paper was included in the following two publications. Theorems in this paper influenced the design of the programming language Dyna developed by Jason Eisner. These theorems also underlie the "rule compiler" used in the implementation of the Ontic verification system.

On the Complexity Analysis of Static Analyses, Static Analysis Workshop, 1999.

On the Complexity Analysis of Static Analyses, JACM, 2002.

Tarskian Set Constraints with Robert Givan and Dexter Kozen, Logic in Computer Science (LICS), 1996.

On the Cubic Bottleneck in Subtyping and Flow Analysis with Nevin Heintze, LICS, 1997.

Linear Time Subtransitive Control Flow Analysis with Nevin Heintze, PLDI, 1997.

The Horn Mu-Calculus with Witold Charatonik, Damian Niwinski, Andreas Podelski, Igor Walukiewicz, LICS, 1998.

An Indexed Model of Recursive Types for Foundational Proof Carying Code with Andrew Appel, TOPLAS, 2001.

Logical Algorithms with Herald Ganzinger, ICLP, 2002.

A Logical Algorithm for ML Type Inference Rewriting Techniques and Applications (RTA), 2003.

A Sound and Complete Model of Contracts with Matthias Blume, ICFP, 2004.

The Generalized A* Architecture with Pedro Felzenszwalb, Journal of Artificial Intelligence Research (JAIR), 2007.