Research

I work (or have worked) on the following:

  • ProofPeer: an ambitious project that aims to establish collaborative theorem proving as a novel paradigm incorporating social computation, interactive theorem proving, and much more.
  • Formal modelling of HIV Care Pathways: This is current work, with Areti Manataki and Petros Papapanagiotou, which involves examining HIV patients’ care in order to provide fully formal, graphical workflows that capture the various processes involved and their composition. This work is done in close collaboration with clinicians from the NHS Greater Glasgow and Clyde and NHS Lothian boards.
  • Mechanical geometry theorem proving: I have looked at novel concepts involving infinitesimal notions in geometry and applied these to the formalization of proofs from Newton’s Principia. I have also worked on the formalization of Hilbert’s Grundlagen and investigated its axiomatics in Isabelle/HOL. The latter is still ongoing work, with Phil Scott and we recently  investigated Hilbert’s (implicit and explicit) reasoning through theorem proving in HOL Light.
  • Formalized mathematics: standard and nonstandard analysis (NSA) in Isabelle/HOL, Many of my mechanized theories are distributed with Isabelle and can be found in the main HOL logic as well as its NSA session. I am currently extending the work and applying it to the mechanization of Euler’s Introductio.
  • Formal Verification of Web Services Composition: This is  work with Petros Papanagiotou that involves producing a framework in HOL Light for verifying the composition of web-services specified in Classical Linear Logic. Through a formalization of the proofs-as-processes paradigm, pi-calculus terms are produced that can then be executed and eventually translated into web-services languages.
  • Concurrent Automated Discovery tools for mathematics: We are developing new systematic ways of integrating discovery with interactive theorem proving. This effort is currently being driven by our work on Hilbert’s geometry although we aim for generic discovery engines.
  • Formal Verification in Computational Geometry: This was work with Laura Meikle on the development of a framework in Isabelle/HOL for reasoning about geometric algorithms. This led to the creation of the Prover’s Palette, which integrates Isabelle, QEPCAD, and Maple within a single IDE based on Eclipse.

Comments are closed.