See the AIML webpage for more up-to-date information. I work (or have worked) on the following:
- Survival Analysis using machine learning and Explainable AI techniques. Projects include predicting graft and patient survival following liver transplantation, in collaboration with Oxford Universities NHS Trusts and data from NHSBT; and looking at brain tumours survival in collaboration with consultant neurosurgeon Paul Brennan.
- Formal modelling in healthcare:
- One project, with Petros Papapanagiotou and Cristina Alexandru, involved 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 work, which looked at long term care, was done in close collaboration with clinicians from the NHS Lothian board. Collaborators on the project includes Areti Manataki and clinicians from NHS Greater Glasgow and Clyde.
- We have also looked at modelling of burns care, patients and handovers transfer in hospitals, and other areas.
- We are now focusing on the use process mining to understand care pathways e.g. to uncover abnormal patterns in ICU patients’ care.
- Formal modelling and verification for manufacturing using WorkflowFM. This was an EIT Digital project (2018-2019) involving the WorkflowFM team consisting of: Petros Papapanagiotou, James Vaughan, Filip Smola 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.