Talks

Title: An overview of the ACRC New Technologies of Care Research plans
Speaker: Jacques Fleuriot and Petros Papapanagiotou
Abstract: The Advanced Care Research Centre (ACRC) is an ambitious £20m research programme funded by Legal and General to look at how care for the person in later life can be improved. It consists of 6 large research workpackages (WP) spanning the social sciences, health and care, artificial intelligence, engineering and much more, and of a PhD academy that will recruit and train 36 students over the next 7 years. The New Technologies of Care WP for its part will aim to develop practical, care-driven technologies that are fit for people in later life. In particular, this will mean exploring and developing sensor-specific data-driven IoT platforms that can produce accurate data about instant events (e.g. vital signs and serious incidents such as falls), short- term activities (e.g. those of daily living) and long-term pursuits (e.g. physical and mental activities over weeks and months) in order to extract (predictive) information and patterns that can be used, among other things, for the prevention of adverse events, adherence to care pathways and effective interventions.

Title: Integrating machine learning and symbolic AI to improve predictive models in healthcare
Speaker: Jorge Gaete
Abstract: The critical nature of medical tasks makes explainability an essential quality of any support system for this domain. Various techniques have been developed to provide explainable ML models for healthcare, nevertheless challenges still exist. Issues such as the integration of multiple sources of information or user interaction with the models are important areas of research to achieve more understandable models. In this talk we introduce our approach to tackling some of these issues by combining current explainable machine learning techniques and symbolic AI. As part of my second-year review, I will present a research pipeline and current work on its implementation and plans for future work. Special attention will be placed on the extraction of clusters as an approach to explain patterns of multimorbidity in patients and also the usage of logic programming to create a simple diabetes risk-predictor.

Title: Computerising Euler's Foundations of Differential Calculus using Nonstandard Analysis
Speaker: Richard Stansfield
Abstract: I will discuss my progress using nonstandard analysis in Isabelle to rigorously formalise of a handful of Euler’s proofs from his Foundations of Differential Calculus. I will walk through an example of this process, highlighting the challenges that Euler's reasoning and Isabelle present and where I am in my project.

Title: Exploring Euler's Differentials of Trigonometric Functions in Isabelle using Nonstandard Analysis
Speaker: Alice Johansen
Abstract: In 1755, Euler published 'Foundations of Differential Calculus' which presented and defined theories of differential calculus. While influential, Euler's text has been criticized by many for lacking rigour, particularily when it comes to his treatment of infinitesimal numbers. For my project, I've attempted to formulate Euler’s reasoning in a rigourous setting, using Isabelle with nonstandard analysis. Isabelle with nonstandard analysis has been a powerful tool for this project, where my goal is to understand how Euler's proofs must be adapted and elaborated upon in order to maintain rigour and consistency. My project focuses on Euler's proofs of the differentials of trigonometric functions, which require consideration when replicated in Isabelle due to their domains and relationships.

Title: Detection of time needed to find study space in the Main Library using Wi-Fi data
Speaker: Dimitris Christodoulou
Abstract: Finding empty space to study in the Main Library can be challenging, particularly in busy periods such as during exams. The aim of this project is to analyse Wi-Fi data in an effort to detect movement patterns in the Library and identify users that eventually settle down in a particular study space. I will describe the progress made on the project so far and outline what remains to be done for the completion of the project.

Title: Developing a New Web Application for the Archive of Formal Proofs
Speaker: Carlin Mackenzie
Abstract:

The Archive of Formal Proofs is functional, however it has not visually changed in almost twenty years. My project aims to rectify this and bring the AFP into the modern day. Previously, I have recreated the website in a more robust static site generator.

Since my last presentation, I have redesigned the user interface, improved discoverability and enhanced code browsing. For each of these, I will explain my approach and demonstrate the latest iteration. Finally, I will present a timeline for the remaining work.

Title: Enhancing Simulation Capabilities in Proter
Speaker: Michal Baczun
Abstract:

Although requirements and criteria for a business process simulator are not fully standardised, there exist a number of commonly expected features and capabilities in the literature. In this talk I will discuss my work towards identifying and implementing some of these capabilities into the existing WorkflowFM Proter simulator. The goal is to assert Proter as a fully capable and highly expressive simulator in order to promote its unique features and capabilities. This includes introducing an interface for the BPMN modelling notation which is used commonly across other simulators.

Title: Resource Aware Process Models
Speaker: Petros Papapanagiotou
Abstract:

Most process modelling languages in use today, including BPMN, Petri Nets, and process calculi, focus on the sequence of activities and the control flow between them. While this allows a variety of qualitative analysis on operational aspects of the process model, quantitative analysis (for instance involving resources) requires separate models and methodologies.

In this talk, I will summarize the main traditional and modern approaches to integrate reasoning about resources in process models. I will focus on the perspectives of 2 separate research fields: Business Process Management and Type Theory and summarize my research plans for correct-by-construction resource aware process models.

Title: Conceptual Integration Networks in Isabelle
Speaker: James Vaughan
Abstract:

Conceptual Integration or Blending is a general cognitive operation used in Linguistics to explain numerous cognitive abilities; from the abstract and metaphorical to the mundane and routine. Spectacular examples of blending in Mathematics, such as Category or Group theory, highlight the power of the process but obscure how ubiquitous it is in human reasoning. I'd like to talk about the network topology of various kinds of conceptual blending and how we can use them to map out mathematical networks within Isabelle.

Title: Compositional Backpropagation
Speaker: Filip Smola
Abstract:

In this talk I will first give an overview of the paper "Backprop as Functor: A compositional perspective on supervised learning" by Fong, Spivak and Tuyéras. This paper takes a structural perspective on backpropagation, giving a functor that converts any differentiable parametrised function into a supervised learning algorithm in a compositional way. With this we can for example factor neural networks into subunits that are simpler to analyse, and more interestingly we can do this in more complex ways than simply by layers. I will then give an overview of our progress mechanising the contents of the paper in Isabelle and describe some of the interesting problems we have faced so far.