The core team members are Richard Bornat, Adam Eppendahl, Samin Ishtiaq, Paul Levy, Peter O'Hearn, David Pym (site representative) Edmund Robinson and Hayo Thielecke, although there are many other researchers in the Faculty, such as Vladimiro Sassone, Peter Landin and Wilfrid Hodges, whose work is of great interest to the team.
The Queen Mary team has been very active in TYPES-related areas.
O'Hearn, Levy and Thielecke have been working on a variety of topics related to continuations, including classical logic, game models, categorical models and basic calculi of continuations and coroutines.
Robinson and Eppendahl have been concerned with categorical models of recursive types and Taylor has developed categorical accounts of well-foundedness, induction and recursion. Taylor has also worked in synthetic domain theory, with the result that domain theory can be extended to synthetic accounts of locally compact spaces.
O'Hearn and Pym, both independently and collaboratively, have worked on aspects of relevant logic and its significance in the semantics of computation. In particular, they have shown that a simple logic of bunches, in which an intuitionistic and linear implication live side-by-side and which has elegant models in a single category with two closed structures, provides an elegant account of sharing in both Idealized Algol and logic programming modules.
Ishtiaq and Pym have developed a new logical framework, RLF. RLF is a conservative extension of LF which is able to uniformly encode a family of weak logics, as well as type systems such as ML with references. This work solves the problem of giving a dependent type theory with a full linear dependent function space. It builds on ideas first presented by Pym at the 1992 Types for Proofs and Programs Workshop in Baastad. Recent work on this topic has focussed on categorical models and proof theory.
Bornat and Ishtiaq both attended the TYPES Workshop in Aussois. Ishtiaq gave a talk on his joint work with Pym on ``A relevant analysis of natural deduction'', and a paper on this topic will shortly appear in the Journal of Logic and Computation. Bornat presented his JAPE proof editor, on which work continues in collaboration with Sufrin of the Oxford site.
Pym, Wallen (Oxford site) and Ritter (Birmingham site) have exchanged several visits. They have been working on various aspects of proof-search in classical and intuitionistic logics, leading to the publication of papers in both the Tableaux and CADE proceedings. Of particular interest to the London group is Pym and Ritter's work on the semantics of classical disjunction and its connections with continuations semantics, with applications to the semantics of logic programming. O'Hearn and Robinson have both visited Birmingham and O'Hearn and Pym have visited Edinburgh. Power (Edinburgh site) has visited London. Bornat has visited Oxford.