Immediately before moving to the University of Strathclyde, I was an Associate Professor in the Computer Science Department at Rutgers University, where I taught computer science courses and pursued research in programming languages. I went to Rutgers from the Mathematics and Computer Science Department at Dickinson College in Carlisle, Pennsylvania, in which I was an Assistant Professor, and to Dickinson from Maine, where I was an Assistant Professor in the Mathematics Department at Bates College in Lewiston. In addition to pursuing PL research and teaching computer science (and, occasionally, mathematics) courses at Dickinson and Bates, I also directed Bates' computer science program. Before that, I was a Research Associate at the Pacific Software Research Center (PacSoft) of the Department of Computer Science and Engineering at the Oregon Graduate Institute of Science and Technology (OGI). There I worked with John Launchbury and Jeff Lewis to implement and study properties of automatable transformation-based methods --- such as short cut fusion --- for improving the efficiency of functional programs. I also finished writing the book Deduction Systems, co-authored with Rolf Socher-Ambrosius.

Prior to joining PacSoft, I was an Assistant Professor in the Department of Mathematics and Computer Science at Hobart and William Smith Colleges (HWS). At HWS I taught both mathematics and computer science courses --- integral and differential calculus, Pascal programming, discrete math, real analysis, topology, automata theory, and algorithmic graph theory, to name a few --- and directed an independent study in equational unification. I also researched lambda calculus- and combinatory logic-based order-sorted higher-order unification algorithms and methods for solving simplification ordering constraints, although this was mostly done during a sixteen-month leave I spent with AG Siekmann at the Universitaet des Saarlandes in Saarbruecken, Germany. These research projects naturally out of my dissertation work --- directed by Dan Dougherty (now at WPI) at Wesleyan University --- on equational and higher-order equational unification. I now find it strange to recall that when I started graduate school I wanted to become an algebraist. But that was before I had encountered theoretical computer science, Church's amazing lambda calculus, or Curry's computationally equivalent combinatory logic.

Theoretical and practical aspects of short cut fusion and similar program transformations remain a strong research interest of mine. Some time ago, I investigated the effectiveness of these fusion techniques in practice with Franklyn Turbak in the Lumberjack Project, and worked with Eelco Visser to adapt them to the strategy language Stratego. I am extremely interested in the role parametricity plays in proving the correctness of short cut fusion and other "free theorems" for various calculi approximating modern functional languages. Subsequent work, done mainly with Janis Voigtlaender, was largely concerned with this issue. The main focus of my research in the late '00s and early '10s was the theory of advanced data types, such as arbitrary inductive types, nested types, GADTs, and dependent types. This work was aimed at developing a deep understanding of the programming constructs (folds, builds, Church encodings, fold/build rules) and reasoning principles (e.g., induction rules) that are supported by initial algebra semantics for such data types. It was conducted primarily with Neil Ghani, but also involved Tarmo Uustalu, Varmo Vene, Bob Atkey, and Clement Fumex. A second line of recent research gives an operational metatheory for Plotkin and Power 's operational effects, and was carried out in collaboration with Alex Simpson and Janis Voigtlaender. Additional work on effectful computation was conducted with Bob Atkey, Neil Ghani, and Bart Jacobs.

Since moving back to the US I have mainly been working on extensions of bifibrational parametricity and the semantics of advanced data types. The former involves Clement Aubert and Kristina Sojakova. The basic theory of bifibrational parametricity for System F was developed jointly with Neil Ghani, Fredrik Nordvall Forsberg, Federico Orsanigo, and Tim Revell at the Mathematically Structured Programming group at the University of Strathclyde. Clement Aubert and I worked on extending the basic theory of bifibrational parametricity to System F with effects. Kristina Sojakova and I have extended the basic theory of bifibrational parametricity to a theory of higher-dimensional parametricity for System F. Andrew Polonsky and I developed a syntax and an initial algebra semantics for GADTs. We then used (a special case of) this semantics as the basis for a theory of (what we call) deep induction for nested data types, which allowed us to (among other things) give the first-ever useful induction rules for the truly nested type of bushes. Enrico Ghiorzi and Daniel Jeffries and I used the fragment of this semantics for nested types to develop a theory of parametricity for a language supporting those types as well, and Enrico and I also developed a theory of (deep) induction for GADTs. I am currently working on a properly functorial initial algebra semantics for GADTs together with Pierre Cagne. A key requirement is that this semantics will subsume the usual initial algebra semantics for ADTs and nested types. This turns out to be quite a challenging problem. Indeed, GADTs are, by design, not functorial over the category of sets, so a setting in which they are functorial is not immediately apparent.

Finally, I did some work on coinductive logic programming with Katya Komendantskaya and her research group at the School of Mathematical and Computer Sciences at Heriot-Watt University (formerly at the School of Computing at the University of Dundee).