Some Research Projects

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.

Two-way Bridge Between Language and Logic

Our system provides a robust, broad-coverage mapping between natural language strings and abstract Knowledge Representation. The forward mapping uses the XLE parser and English ParGram grammar, followed by semantic and AKR rules using XLE's ordered rewrite system (XFR). This process is reversed for generation of grammatical, natural language strings from AKR. This Aquaint II  project began in May 2004 and ended October 2006.

Hybrid Logic Meets Other Logics (HyLoMOL)

Hybrid logic is a branch of modal logic in which it is possible to directly refer to worlds/times/states or whatever the elements of the (Kripke) model are meant to represent. I'm particularly interested in constructive versions of  hybrid logics. The project HyLoMOL is funded by the 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.

Intuitionistic Modal Logics

 Informal research project with several collaborators, including Torben Brauner, Gianluigi Bellin, Eike Ritter, Michael Mendler, Rajeev Gore, Natasha Alechina, Frank Pfenning, Neil Ghani and Milly Maietti. Some of my reasons for being interested in intuitionistic modal logics are described in the 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.

Identity of Proofs

A small project with Luiz Carlos Pereira and Hermann Hausler on uses of Category Theory to distinguish proofs. Started  2005.

Other Projects

xSLAM: an abstract machine for Linear Functional Programming
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.