Skip to content

Publication

Our new paper on chronic illnesses and depression featured in UKRI news

    Our new paper, Cluster and survival analysis of UK biobank data reveals associations between physical multimorbidity clusters and subsequent depression, has just been published in Nature Communications Medicine. The results have been highlighted by the MRC on the UKRI website and featured in its newsletter. See:

    UKRI News: https://www.ukri.org/news/multiple-chronic-illnesses-linked-to-higher-risk-of-depression
    Edinburgh University post: https://www.ed.ac.uk/news/multiple-chronic-illnesses-could-double-risk-of-depression

    and

    Full paper at: https://doi.org/10.1038/s43856-025-00825-7
    Code at: https://github.com/laurendelong21/clusterMed

    Our paper “Linear Resources in Isabelle/HOL” has just been published in the Journal of Automated Reasoning

      Abstract:

      We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of these compositions is verified by translating them into deductions in intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction when satisfied. We mechanise the whole framework, including a deep embedding of ILL, in the proof assistant Isabelle/HOL. Beyond the increased confidence in our proofs, this allows us to automatically generate executable code for our verified definitions. We demonstrate our approach by formalising part of the simulation game Factorio and modelling a manufacturing process in it. Our framework guarantees that this model is free of bottlenecks.

      Smola, F., Fleuriot, J.D. Linear Resources in Isabelle/HOL. J Autom Reasoning 68, 9 (2024). https://doi.org/10.1007/s10817-024-09698-2