Talks

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.

Title: Automated HOL Light Theorem Annotation
Speaker: Timmy Gill
Abstract:

This talk will introduce my work looking to find ways to tag theorems in HOL Light corpora with their associated areas of mathematics. It is hoped that this will enhance users' ability to understand theorems, quickly find groups of related theorems and more easily navigate libraries to find relevant lemmas for proofs. I will introduce some of the methods I propose to use to generate/ propagate tags and
describe the intuition for using them in this context.

Title: Looking Ahead in Discrete Event Simulation
Speaker: Michal Baczun
Abstract:

Discrete event simulation is a common method for analysing business processes for the purposes of predictive analytics, optimisation, and exploring possible “what-if” scenarios. Modelling a process and its environment with the appropriate level of detail for the purposes of the simulation can be challenging, and often simulations cannot support certain features of a process. One such example is the prioritisation of tasks, and scheduling that considers the priorities of not only current but also future tasks. In this presentation I will discuss the value of look-ahead functionality in workflow simulation, and how we have incorporated look-ahead capabilities into an existing discrete event simulation environment, namely WorkflowFM.