I work (or have worked) on the following:
- Formal modelling in healthcare: One current project, with Petros Papapanagiotou and Cristina Alexandru, involves examining HIV patients’ care in order to provide fully formal, graphical workflows that capture the various processes involved in HIV Integrated Care Pathways (ICPs). The current work, which is looking at long term care, is done in close collaboration with clinicians from the NHS Lothian board. Past collaborators on the project included Areti Manataki and clinicians from NHS Greater Glasgow and Clyde.
- Formal modelling and verification for manufacturing using WorkflowFM. This is an EIT Digital project involving Petros Papapanagiotou and myself.
- ProofPeer: an ambitious project that aims to establish collaborative theorem proving as a novel paradigm incorporating social computation, interactive theorem proving, and much more.
- 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. Phil Scott, as part of his PhD under my supervision, 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.