{"id":201,"date":"2011-06-16T21:53:39","date_gmt":"2011-06-16T21:53:39","guid":{"rendered":"http:\/\/homepages.inf.ed.ac.uk\/jdf\/?page_id=201"},"modified":"2024-05-12T13:53:50","modified_gmt":"2024-05-12T13:53:50","slug":"research","status":"publish","type":"page","link":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/research\/","title":{"rendered":"Research"},"content":{"rendered":"<p>See the\u00a0<a href=\"https:\/\/aiml.inf.ed.ac.uk\">AIML<\/a> webpage for more up-to-date information. I work (or have worked) on the following:<\/p>\n<ul>\n<li>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 <a href=\"https:\/\/www.nhsbt.nhs.uk\">NHSBT<\/a>; and looking at brain tumours survival in collaboration with consultant neurosurgeon\u00a0<a href=\"https:\/\/www.ed.ac.uk\/profile\/dr-paul-brennan\">Paul Brennan<\/a>.<\/li>\n<li>Formal modelling in healthcare:\n<ul>\n<li>One project, with\u00a0<a href=\"http:\/\/www.inf.ed.ac.uk\/people\/students\/Petros_Papapanagiotou.html\">Petros Papapanagiotou<\/a>\u00a0and Cristina Alexandru, involved examining HIV patients&#8217; care in order to\u00a0provide 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.\u00a0Collaborators on the project includes\u00a0<a href=\"http:\/\/homepages.inf.ed.ac.uk\/s0675919\/\">Areti Manataki<\/a>\u00a0and\u00a0clinicians from NHS Greater Glasgow and Clyde.<\/li>\n<li>We have also looked at modelling of burns care, patients and handovers transfer in hospitals, and other areas.<\/li>\n<li>We are now focusing on the use process mining to understand care pathways e.g. to uncover abnormal patterns in ICU patients&#8217; care.<\/li>\n<\/ul>\n<\/li>\n<li>Formal modelling and verification for manufacturing using <a href=\"http:\/\/www.workflowfm.com\">WorkflowFM<\/a>. This was an EIT Digital project (2018-2019) involving the WorkflowFM team consisting of:\u00a0<a href=\"http:\/\/www.inf.ed.ac.uk\/people\/students\/Petros_Papapanagiotou.html\">Petros Papapanagiotou<\/a>, James Vaughan, Filip Smola and myself.<\/li>\n<li><a href=\"http:\/\/www.proofpeer.net\">ProofPeer<\/a>:\u00a0an ambitious project that aims to establish collaborative theorem proving as a novel\u00a0paradigm incorporating social computation, interactive theorem proving, and much more.<\/li>\n<li>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&#8217;s\u00a0<em>Principia<\/em>. I have also worked on the formalization of Hilbert&#8217;s <a title=\"Hilbert's Foundations of Geometry\" href=\"http:\/\/en.wikipedia.org\/wiki\/Hilbert%27s_axioms\"><em>Grundlagen<\/em><\/a> and investigated its axiomatics in Isabelle\/HOL. <a href=\"http:\/\/www.inf.ed.ac.uk\/people\/students\/Phil_Scott.html\" rel=\"nofollow\">Phil Scott,\u00a0<\/a>as part of his PhD under my supervision, recently \u00a0investigated Hilbert&#8217;s (implicit and explicit) reasoning through theorem proving in HOL Light.<\/li>\n<li>Formalized mathematics: standard and nonstandard analysis (NSA) in\u00a0<a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\" rel=\"nofollow\">Isabelle<\/a>\/HOL, Many of my mechanized theories are distributed with Isabelle and can be found in the main\u00a0<a href=\"http:\/\/isabelle.in.tum.de\/dist\/library\/HOL\/index.html\" rel=\"nofollow\">HOL<\/a> logic as well as its\u00a0<a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/library\/HOL\/HOL-Nonstandard_Analysis\/index.html\" rel=\"nofollow\">NSA<\/a> session. I am currently extending the work and applying it to the mechanization of Euler&#8217;s <em>Introductio<\/em>.<\/li>\n<li>Formal Verification of Web Services Composition: This is \u00a0work with <a href=\"http:\/\/www.inf.ed.ac.uk\/people\/students\/Petros_Papapanagiotou.html\" rel=\"nofollow\">Petros Papanagiotou<\/a> 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.<\/li>\n<li>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&#8217;s geometry although we aim for generic discovery engines.<\/li>\n<li>Formal Verification in Computational Geometry: This was work with\u00a0<a href=\"http:\/\/www.inf.ed.ac.uk\/people\/students\/Laura_Meikle.html\" rel=\"nofollow\">Laura Meikle<\/a> on the development of a\u00a0<a href=\"http:\/\/homepages.inf.ed.ac.uk\/s9811254\" rel=\"nofollow\">framework<\/a> in Isabelle\/HOL for reasoning about geometric algorithms. This led to the creation of the Prover&#8217;s Palette, which integrates Isabelle,\u00a0<a href=\"http:\/\/www.usna.edu\/Users\/cs\/qepcad\/B\/QEPCAD.html\" rel=\"nofollow\">QEPCAD<\/a>, and\u00a0<a href=\"http:\/\/www.maplesoft.com\/products\/maple\" rel=\"nofollow\">Maple<\/a> within a single IDE based on\u00a0<a href=\"http:\/\/www.eclipse.org\/\" rel=\"nofollow\">Eclipse<\/a>.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>See the\u00a0AIML 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 &hellip; <a href=\"https:\/\/homepages.inf.ed.ac.uk\/jdf\/research\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":204,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-201","page","type-page","status-publish","has-post-thumbnail","hentry"],"_links":{"self":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/201","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/comments?post=201"}],"version-history":[{"count":25,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/201\/revisions"}],"predecessor-version":[{"id":531,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/201\/revisions\/531"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/media\/204"}],"wp:attachment":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/media?parent=201"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}