The following are some of my main research interests:
- Automated theorem proving in substructural logics, such as linear logic
- Proof theory, particularly that of Gentzen’s sequent calculus
- Formal verification of software specifications
- Universal proof languages
My long term goal is much more pragmatic than scientific: I want to improve—perhaps restore—our faith in software. This can only be achieved by giving software creators the means to specify, precisely and formally, and with a minimum amount of annoyance, the intended behaviour of software components, and then to check that the software they write conforms to these specifications. Automation is critical in every step of this kind of engineering. Programmers are generally not logicians, nor are they renowned for their patience. I will consider my goals sufficiently achieved if specification and verification is done as a matter of course, just as type systems are used today as a matter of course to guard against well known conceptual and linguistic errors in programming.