Under development.
My research links logic and computer science, often using the technology of category theory, sometimes overtly, sometimes covertly.
Most of my recent work has been on the combinatorial structure of mathematical proofs. I was able to extend a net-theoretic formalism from sub-structural logic to full classical logic, an extension that was previously believed to be impossible. This formalism removes inessential choices about the ordering of stages in the proof and hence allows a more canonical representation.
I began my research career in Mathematics, using categorical and logical techniques to investigate the properties of equationally defined sets over p-adically closed number fields. I then moved to Edinburgh, where my brief was to help people there who needed to know more Category Theory. I exploited the opportunity to learn some Computer Science.
On my return to Cambridge, I began work aimed at exploiting the duality between lattices of propositions and topological spaces in order to set up programming logics. This is comparable to Abramsky’s program for “Domain Theory in Logical Form”. Hyland and I obtained a SERC grant to employ Rosolini, and on his arrival in Cambridge I got caught up in a program to use the Effective Topos to model various polymorphic calculi. In particular we were able to give a sharp characterization of the completeness properties of one small subcategory of the topos. This enabled us to unify the construction of models for several different calculi, and also to construct models for new calculi very quickly.
I continued working in much the same area during my stay in Canada, but with more emphasis on finding the non-standard properties of the model. In particular, we hoped that it would provide a model of a “parametric” form of the calculus. We were able, with difficulty to prove that this was indeed so for types of a relatively low order, but now suspect that a general result is false. These were the best model-theoretic results on parametricity of their time. In some more recent work I have moved much more in the direction of an investigation of parametricity (that, in fact is the purpose of my Advanced Fellowship). There are various approaches to the notion of parametricity (intended to distinguish uniform definitions, from ones which depend on types in an ad hoc fashion), but in my view the most significant is the one due to Reynolds, which links it to data abstraction. Put simply, Reynolds idea is that if polymorphic functions had different semantics at different types, then we could make use of that to distinguish between different implementations of supposedly abstract types. Of course, from this point of view, different degrees of abstraction require differing degrees of parametricity, and my paper on “Parametricity as Isomorphism” is a complete account of the connection in a low-grade situation. I am working on improving this to more refined notions of abstraction.
My LICS paper with Rosolini shows that (under fairly mild assumptions) it is possible to extract a parametric model of the second order lambda calculus from a non-parametric one (here parametricity is interpreted as meaning “respecting logical relations”). This gives us for the first time a rich supply of parametric models. But, interestingly, we can vary the notion of parametricity here, too. The Birmingham paper carriees on with the theme, and I show that a certain type of logical relation is sound and complete for data abstraction for higher-order theories, extending a result previously only known at first-order.
I have also been involved in a project with John Power on a notion called premonoidal categories. Our work is aimed at providing a new categorical framework to describe the connection between the semantics of a type theory, and the semantics of the programming languages that might be based upon it. The most recent work is embodied in the paper on “Modularity and dyads”. This paper contains a complete account of a mathematical theory aimed at solving some of the difficulties faced by compiler writers trying to write modular compilers.