{"id":14,"date":"2011-05-26T18:47:56","date_gmt":"2011-05-26T18:47:56","guid":{"rendered":"http:\/\/homepages.inf.ed.ac.uk\/jdf\/?page_id=14"},"modified":"2026-02-26T17:04:19","modified_gmt":"2026-02-26T17:04:19","slug":"students","status":"publish","type":"page","link":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/students\/","title":{"rendered":"Students"},"content":{"rendered":"<p><span style=\"font-family: Georgia, 'Bitstream Charter', serif; line-height: 24px; font-size: 16px;\">Current PhD Students (Principal Supervisor)<\/span><\/p>\n<ul>\n<li>Zonglin Ji (<em>AI \u00a0for healthcare processes<\/em>)<\/li>\n<li>Alex Hyman<\/li>\n<\/ul>\n<p><span style=\"font-family: Georgia, 'Bitstream Charter', serif; line-height: 24px; font-size: 16px;\">Recent Masters Students<\/span><\/p>\n<ul>\n<li>Matt Whyte (2023, <em>Formalising Tensors in Isabelle\/HOL &#8211; A Neurosymbolic Pipeline from Formal Specifications to Efficient Machine Learning Code, <strong>passed with Distinction<\/strong><\/em>). One of the <strong>outstanding<\/strong> MSc theses of the academic year 2022-23.<\/li>\n<li>Scott O\u2019Donoghue (2022,\u00a0<em>Applying Machine Learning and Interpretable Techniques to Persistent Critical Illness, <strong>passed with Distinction<\/strong><\/em>). In collaboration with Naz Lone, Anaesthesia, Critical Care and Pain Medicine, Usher Institute.<\/li>\n<li>Callum Abbott (2021,<i>\u00a0 To Drain or Not to Drain? A Causal Investigation into the Efficacy of Subdural Drains in Preventing CSDH Recurrence, <em><strong>passed with Distinction<\/strong><\/em><\/i>). <strong>Winner<\/strong> of the MSc in Data Science prize in the School of Mathematics. In collaboration with Paul Brennan and Michael Poon, Centre for Clinical Brain Sciences.<\/li>\n<li>Mathis Gerdes (2021, <em><span dir=\"ltr\" role=\"presentation\">A Mechanized Investigation of an\u00a0<\/span><span dir=\"ltr\" role=\"presentation\">Axiomatic System for Minkowski\u00a0<\/span><span dir=\"ltr\" role=\"presentation\">Spacetime, <strong>passed with Distinction<\/strong><\/span><\/em>), one of the <strong><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/2021-outstanding.html\">outstanding<\/a><\/strong> level MSc theses of the academic year 2020-21.<\/li>\n<li>Richard Schmoetten (2020,\u00a0<em>Mechanizing Minkowski spacetime, <strong>passed with Distinction<\/strong><\/em>).\u00a0One of the <a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/2020-outstanding.html\"><strong>outstanding<\/strong><\/a> MSc theses of the academic year 2019-20 and <strong>Winner<\/strong> of the MSc in Informatics thesis prize.<\/li>\n<li>Colleen Charlton (2020,\u00a0<em>Interpretable Classifiers for Brain Tumour Prediction, <strong>passed with Distinction<\/strong><\/em>).\u00a0In collaboration with Paul Brennan and Michael Poon, Centre for Clinical Brain Sciences, University of Edinburgh. One of the <a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/2020-outstanding.html\"><strong>outstanding<\/strong><\/a> MSc theses of the academic year 2019-20.<\/li>\n<li>Anita Klementiev (2020,\u00a0<em>Process Mining Techniques for Modelling Healthcare Patient Paths, <strong>passed with Distinction<\/strong><\/em>).<\/li>\n<li>Simon Thorogood (2019,\u00a0<em>Machine learning prediction of graft and patient survival following liver transplantation, <strong>passed with Distinction<\/strong><\/em>). In collaboration with Oxford NHS Trusts and NHSBT. One of the <strong><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/2019-outstanding.html\">outstanding<\/a><\/strong> MSc theses of the academic year 2018-19 and <strong>Winner<\/strong> of the MSc in Data Science thesis prize.<\/li>\n<li>Callum Biggs O&#8217;May (2019, M<em>achine learning based survival analysis for brain tumours, <strong>passed with Distinction<\/strong><\/em>). In collaboration with the\u00a0Paul Brennan, Centre for Clinical Brain Sciences, University of Edinburgh.Edinburgh.\u00a0One of the <strong><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/2019-outstanding.html\">outstanding<\/a><\/strong> MSc theses of academic year 2018-19.<\/li>\n<li>Jessika Rockel (2019,\u00a0<em>Formalization of proofs from Euler&#8217;s Differential Calculus in Isabelle, <strong>passed with Distinction<\/strong><\/em>).\u00a0 One of the <strong><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/2019-outstanding.html\">outstanding<\/a><\/strong> MSc theses of academic year 2018-19.<\/li>\n<li>Ka Wing Pang (2019,\u00a0<em>Coinductive reasoning over streams in Isabelle\/HOL, <strong>passed with Distinction<\/strong><\/em>).<\/li>\n<\/ul>\n<p><span style=\"font-family: Georgia, 'Bitstream Charter', serif; line-height: 24px; font-size: 16px;\">Recent Interns<\/span><\/p>\n<ul>\n<li>Alex Hyman (2023, <em>Formal Verification of \u00a0Automatic Differentiation<\/em>).<\/li>\n<li>Matthew Whyte (2022-23, <em>Formally-constrained Neural Learning<\/em>).<\/li>\n<li>Filip Smola (2020,\u00a0<em>Interactive theorem proving and formal verification, with application to automatic differentiation<\/em>).<\/li>\n<li>Filip Smola (2019, \u00a0<em>Formal modelling of industrial workflows using Digiflow<\/em>).<\/li>\n<li>Kyriakos Katsamaktsis (2019,\u00a0<a href=\"https:\/\/arxiv.org\/abs\/0905.2254\"><em>Formalization of Euler&#8217;s paper on the infinity of infinities of orders of the infinitely large and infinitely small<\/em><\/a>).<\/li>\n<\/ul>\n<p><span style=\"font-family: Georgia, 'Bitstream Charter', serif; line-height: 24px; font-size: 16px;\">Past PhD Students (Principal Supervisor)<\/span><\/p>\n<ul>\n<li>Richard Schmoetten (<em>Formalisation of axiomatic Quantum Field Theory in Isabelle\/HOL<\/em>)<\/li>\n<li>James Vaughan (<em>Network Analysis for Mathematical Reasoning in Isabelle<\/em>)<\/li>\n<li>Lauren DeLong <em>(Neurosymbolic AI in medicine\/healthcare<\/em>)<\/li>\n<li>Filip Smola (<em>Formal Modelling of Complex Systems via Compositional Approaches in Isabelle\/HOL<\/em>)<\/li>\n<li>Jiawei Zheng (<em>Probabilistic reasoning over processes<\/em>)<\/li>\n<li>Jorge Gaete Villegas (<em>Modelling and Predicting Medical Outcomes for Intensive Care Patients via Network Mechanisms and Machine<br \/>\nLearning<\/em>, 2024).<\/li>\n<li>Mark Chevallier (<em>Applications of Formalised Mathematics and Logic to Reinforcement and Deep Learning, 2023<\/em>).<\/li>\n<li>Imogen Morris (<em>Formalization of Euler&#8217;s Introductio in Isabelle\/HOL, 2022<\/em>).<\/li>\n<li>Jake Palmer (<em>Formal Verification of Voting Algorithms in Isabelle, 2022<\/em>).<\/li>\n<li>Yaqing Jiang (<em>Machine Learning for Inductive Theorem Proving, 2018<\/em>).<\/li>\n<li>Phil Scott \u00a0(<em>Ordered Geometry in Hilbert&#8217;s Grundlagen der Geometrie<\/em>, 2014)<\/li>\n<li>Petros Papapanagiotou\u00a0(<em>A Formal Verification Approach to Process Modelling and Composition<\/em>, 2014)<\/li>\n<li>Laura Meikle (<em>Intuition in Formal Proof: A Novel Framework for Combining Mathematical Tools<\/em>, 2013)<\/li>\n<li>Sean Wilson (<em>Supporting Dependently Typed Functional Programming with Proof Automation and Testin<\/em>g, 2010)<\/li>\n<li>Lucas Dixon (<em>A Proof Planning Framework for Isabelle<\/em>, 2006)<\/li>\n<li>Ewen Maclean (<em>Using Proof-Planning to Investigate the Structure of Proof in Non-Standard Analysis<\/em>, 2003)<\/li>\n<\/ul>\n<p><span style=\"font-family: Georgia, 'Bitstream Charter', serif; line-height: 24px; font-size: 16px;\">Past PhD Students (Second Supervisor, incomplete list)<\/span><\/p>\n<ul>\n<li>Tom Ridge (2005)<\/li>\n<li>Mark Collins (2005)<\/li>\n<li>Zhiheng Huang (2005)<\/li>\n<li>Jeremy Gow (2004)<\/li>\n<\/ul>\n<p><span style=\"font-family: Georgia, 'Bitstream Charter', serif; line-height: 24px; font-size: 16px;\">Past MSc Students (Very incomplete list)<\/span><\/p>\n<ul>\n<li>Victor Dumitrescu (MSc by research, 2016)<\/li>\n<li>Phil Scott (2008)<\/li>\n<li>Petros Papapanagiotou (2007)<\/li>\n<li>Jonas Halvorsen (2007)<\/li>\n<li>Chris Laumann (2004)<\/li>\n<li>Robbert Brak (2004)<\/li>\n<li>&#8230;<\/li>\n<\/ul>\n<p><span style=\"font-family: Georgia, 'Bitstream Charter', serif; line-height: 24px; font-size: 16px;\">Past Undergraduate\u00a0Students<\/span><\/p>\n<ul>\n<li>Too many to mention (but if one of you is reading this: you were all special) \ud83d\ude42<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Current PhD Students (Principal Supervisor) Zonglin Ji (AI \u00a0for healthcare processes) Alex Hyman Recent Masters Students Matt Whyte (2023, Formalising Tensors in Isabelle\/HOL &#8211; A Neurosymbolic Pipeline from Formal Specifications to Efficient Machine Learning Code, passed with Distinction). One of &hellip; <a href=\"https:\/\/homepages.inf.ed.ac.uk\/jdf\/students\/\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":216,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-14","page","type-page","status-publish","has-post-thumbnail","hentry"],"_links":{"self":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/14","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=14"}],"version-history":[{"count":64,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/14\/revisions"}],"predecessor-version":[{"id":533,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/pages\/14\/revisions\/533"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/media\/216"}],"wp:attachment":[{"href":"https:\/\/homepages.inf.ed.ac.uk\/jdf\/wp-json\/wp\/v2\/media?parent=14"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}