Talks

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.

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

The Archive of Formal Proofs is the primary repository for Isabelle formal logic proofs on the internet. It functions as a journal with annual releases and to date over 350 authors have contributed. The AFP is currently functional, however it is very demanding to maintain and unintuitive to browse. This work aims to improve upon the existing AFP by conducting user surveys and using this to guide development in the areas of user experience and maintainability.

Title: Exploring Euler's Differentials of Exponential Functions in Isabelle using Nonstandard Analysis
Speaker: Richard Stansfield
Abstract:

Many of the proofs of important results in analysis from Euler’s Foundations of Differential Calculus have been called into question due to their lack of rigour and reliance on the existence of infinitely small numbers, which standard mathematics now rejects. However, using nonstandard analysis formalised in Isabelle we may now be able to rigorously rehabilitate them and in doing so uncover the implicit reasoning behind some of the legendary mathematician’s results.

In particular, my project will focus on a handful of proofs regarding differentials of functions involving exponentiation. I will talk about the background to the project – hopefully giving an intuitive impression of nonstandard analysis for the unfamiliar – as well as discussing some of the difficulties that arise when converting Euler to Isabelle.

Title: Exploring Euler's Differentials of Trigonometric Functions in Isabelle using Nonstandard Analysis
Speaker: Alice Johansen
Abstract:

In 1755, Euler published his influential 'Foundations of Differential Calculus' which presented and defined theories of differential calculus and discussion of the infinite. While Euler makes missteps and often excludes assumptions in his proofs, one must remember that in context, eighteenth-century mathematicians did not have the same expectations of rigour that one might have today, and thus there is value in formulating Euler’s reasoning now with the diligence that his text lacked. Returning to our current time, interactive proof assistant Isabelle has helped verify countless theorems across mathematics and computer science domains, and I will use this powerful tool to explore and prove Euler's differential definitions for trigonometric functions sin, cos and hopefully more via nonstandard analysis

Title: Detection of the time required 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 WiFi data in an effort to detect movement patterns in the Library and identify users that eventually settle down in a particular study space. This data will then be used to provide indications or predictions of how long it may take to find an empty study space at any given time.