(with Alexandre Rademaker, FGV, Rio de Janeiro, Brazil) Started July 2011.
ASKER Ambiguity-Enabled, Scalableable Knowledge Repository, partially funded by DTO's Advanced Question and Answering for Intelligence (Aquaint 3) program. This project began in Nov 2006 and uses the system Bridge described below.
IKRIS Interoperable Knowledge Representation for Intelligence Support was an 18 month project sponsored by the Disruptive Technology Office (DTO, formerly known as ARDA-Advanced Research and Development Activity). It started in April 2005, and concluded in September 2006.
Danish Natural Science Research Council (2005 - 2007), Brauner is the principal investigator. See also the hybrid logics webpage and program of the workshops, Hylo06 and Hylo07.
preface of the special issue of the Journal of Logic and Computation that I guest edited with Rajeev Gore' and Michael Mendler. Beginnings of a bibliography on constructive modal logics can be found here.
See also the websites for the IMLA workshops in 1999, 2002 and 2005.
Hermann Hausler on uses of Category Theory to distinguish proofs. Started 2005.
Together with Eike Ritter, Neil Ghani (now at Nottingham), Milly Maietti, Francisco Alberti and Paola Maneggia I helped develop xLIN, a linear abstract machine, based on a calculus of explicit substitutions. You can read about this EPSRC project in the xSLAM page. This project finished in March 2000, you can read a short summary here. But there are lots of loose ends and threads that we are still trying to tie-up.
Formal Verification using Subtructural Logics
Together with Saraswati Kalvala and Eike Ritter and Milly Maietti I am thinking about substructural logics for formal verification. This builds on our previous collaboration on mechanising Linear Logic in Isabelle, but the project is "on the back burner" for the time being.
Dialectica Categories and Full Intuitionistic Linear Logic
Together with Torben Brauner, Eike Ritter and Milly Maietti, I started working on building up the foundations of Full Intuitionistic Linear Logic, in principle funded by the Nuffield Foundation. Due to my relocation to the US, the official project was cancelled and the abstract project has been in the "back burner" for a while. But there are lots of things that I still want to do about it, for a summary of applications of the dialectica categories, check this preprint.
Another branch of this work was the special issue of TAC on Chu Spaces: Theory and Applications, vol 17, 2006. Check it out here.