Some Research Projects
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
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.
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
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 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
investigator. See also the hybrid
logics webpage and program of the workshops, Hylo06 and Hylo07.
Intuitionistic Modal Logics
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
Category Theory to distinguish proofs. Started 2005.
xSLAM: an abstract machine for Linear Functional
Together with Eike Ritter,
Neil Ghani (now at
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.