Software
Throughout my career, I have been involved in the development of a number of tools, prototypes, and libraries. Listed below are the ones that have been released as open source software under permissive licenses.
Cats-Actors
2024-today
Cats-Actors 🐱 is a functional programming-based actor system derived from Akka Akka v2.6.21. It is available under the Apache 2.0 License on GitHub: https://github.com/suprnation/cats-actors Description The following text taken from the project README (original author: Mark Galea) introduces Cats-Actors, its main goal and benefits. Introduction Actors are the fundamental units of computation in …
Proter
2019-today
Proter is an open-source discrete event simulation library for workflows, written in Scala. It is part of our WorkflowFM framework for formal workflow modelling and management. It is available under the Apache 2.0 License on GitHub: https://github.com/workflowfm/proter Website and documentation is available here: http://docs.workflowfm.com/proter/ Proter was initially developed for the simulation …
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 …
PEW
2019-2022
PEW is a persistent execution engine for π-calculus workflows generated by the WorkflowFM process composition tools, written in Scala. It is part of our WorkflowFM framework for formal workflow modelling and management. It is available under the Apache 2.0 License on GitHub: https://github.com/workflowfm/pew Website and documentation is available here: http://docs.workflowfm.com/pew/
WorkflowFM Composer
2009-2022
The WorkflowFM Composer is a a diagrammatic tool for formally verified process modelling and composition. It is available under the Apache 2.0 License on GitHub: https://github.com/workflowfm/workflowfm-composer Website and documentation is available here: http://docs.workflowfm.com/workflowfm-composer/ About The WorkflowFM Composer consists of a Java-based server and GUI for formally verified …
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 …
Other minor software:
- Healthcare Handover: Workflow simulation of patient handovers (assignment/delegation) between medical staff, based on this project.
- d3-workflow-timeline: An adaptation of d3-timeline to display workflow and simulation data for WorkflowFM.
- Proter Tutorial: A simple example project for the Proter business process simulator, involving serving pizza and garlic bread.
- SubAkka: A (not very successful) one-to-many pub/sub pattern in Scala using Akka.