Hol light

Logic-based workflows

2009-today

This project aims to enhance the development of process workflows with AI techniques so that various properties of the models are verified as they are being built, i.e. workflows that are correct-by-construction. In particular, we employ the proofs-as-processes paradigm which describes the correspondence between Classical Linear Logic (CLL) proofs with π-calculus processes. This enables us to …

WorkflowFM Reasoner

2009-2022

The WorkflowFM Reasoner is a logic-based library for correct-by-construction process modelling and composition. It is available under the Apache 2.0 License on GitHub: https://github.com/workflowfm/workflowfm-reasoner Website and documentation is available here: http://docs.workflowfm.com/workflowfm-reasoner/ About It is implemented as a logic-based library for the interactive theorem prover HOL …

HOL Light Embed

2019-2020

I have developed a generic framework to perform object level reasoning with embedded logics in HOL Light. It provides procedural tactics inspired by Isabelle’s rule/erule/drule/frule. It also supports correspondences with computational terms in the style of Curry-Howard. It is available under the BSD-3-Clause License on GitHub: https://github.com/PetrosPapapa/hol-light-embed Additional …

Isabelle Light

2009-2018

HOL Light is a modern theorem proving system characterised by its powerful, low level interface that allows for flexibility and programmability. However, considerable effort is required to become accustomed to the system and to reach a point where one can comfortably achieve simple natural deduction proofs. Isabelle is another powerful and widely used theorem prover that provides useful features …

Boyer-Moore

2006-2017

In this project, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. Based on the concepts and methodology underlying this 40-year-old model, we have implemented a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic. We have also included several extensions and enhancements to …

HOL Light Tools

2014-2019

This is a library of tools, tactics, and theories I have developed in HOL Light. Some of these, such as the finite map theory, have been ported from the work of others, particularly in HOL4. Notable things included: A port of the finite map theory from HOL4. A set of tools to enable proofs in an arbitrarily extended proof state. A small library about substitution. Additional definitions and lemmas …

SOCIAM

2014-2018

SOCIAM was an EPSRC funded project involving the Universities of Oxford, Edinburgh and Southampton, focusing on the theory and practice of social machines. The following slideshare gives an overview of social machines and SOCIAM: {{< slideshare id=“jogOZAD0VgkoJj” >}} The official website contains detailed information about the numerous aspects, research topics, outputs, and …

Integrated Care Pathways for HIV patients

2014-2018

We work in close collaboration with the NHS Lothian and NHS Greater Glasgow and Clyde boards to improve HIV care by mapping the processes involved in the form of an Integrated Care Pathways (ICPs). We employ a rigorous methodology involving contextual interviews, questionnaires, and shadowing to capture the and record necessary knowledge. Using the logic-based tool WorkflowFM for this purpose …

Lightweight Social Calculus

2014-2018

We would like to change the way in which social machines are built. The central premise is: there is a model of interaction which sits behind any social machine, governing who can do what when, which kinds of messages can be sent and to whom, shaping the ways in which the complex socio-technical system unfolds through time. However, these interaction models are often not explicit, transparent, …