Interests
Generally speaking my research interests involve making Systems Engineering more TyDe: Type-Driven. I want to combine state-of-the-art programming language theory, namely from type-systems, dependent types & functional programming, and fundamentally change the way we engineer systems by interlinking our System’s specifications and implementations. I believe that if we are to ever build trustworthy systems, we must make machine checkable specifications an intrinsic aspect of the system through adoption of type-driven approaches. There are more topics (privacy and cryptography) that I am interested in, but the above keeps me busy for now!
Vision
The security of our Digital Technologies is paramount as Society and the Economy becomes evermore digital. Fundamentally, there is a separation-of-concerns between system: specification—by domain experts; verification—by verification experts; creation—by software engineers; use—by end users; and certification—by auditors. Such a disconnect leads to issues over system trustworthiness by allowing potentially exploitable vulnerabilities and errors to be present at various points during a system’s lifecycle.
Type-Driven (TyDe) techniques see the creation of expressive type systems to capture the structural and behavioural specifications our programs have. It is through the type checking process that we can provide static design time guarantees that a system does indeed follow its specification. Through adoption of TyDe techniques we can: reduce mismatches between a system’s specification and implementation; increase productivity of system creation and verification; and fundamentally enhance system trustworthiness. This will benefit both Society and the Economy by guaranteeing that our systems are trustworthy because our engineering practises are also trustworthy.
In Welsh English the word ‘tidy’ describes anything that is positive, good, neat. . . . I want to make engineering tidy. What better way of doing so by making our engineering practices: Type-Driven!
Projects
AppControl is an EPSRC funded research project that is part of the Industrial Strategy Challenge Fund: Digital Security by Design. The project is a collaboration between the Universities of Glasgow, Imperial College London, and Essex. This project’s goal is to improve upon the trustworthiness of Hardware/Software Co-Design by combining the results of Border Patrol with that of Capability Hardware as developed by the CHERI Program.
Border Patrol is an EPSRC funded research project that is part of the Trust, Identity, Privacy and Security in the Digital Economy call. The project is a collaboration project between the Universities of Glasgow, Heriot-Watt, and Imperial College London. The project’s goal is to make the design of hardware systems, and in particular smart devices, resiliant against hidden malicious functionality by ensuring that devices only do what is expected of them. It is an ambitious project that combines state-of-the-art advances in type theory and compiler technology, and applies them to hardware design.
Idris is a general purpose dependently typed language. I have been involved with the project for many years as developer and community participant. I help administer the Github project pages for the compiler and community.
Ola is a personal project that sees me try and implement reference implementations of different styles of programming languages within Idris2. Mostly for pedagogical reasons. I have not seen reasons to write them up as academic papers. So far there have been two ‘main’ languages: Olaf & Olai.
Previous Projects
Security by Design and Construction was a six-month project looking at type-driven verification of communicating systems. I was employed as an RA to investigate how to use dependent types and algebraic effect handlers to reason about communicating systems.
Type-Driven Verification of Communicating Systems was a one year EPSRC first grant to investigate the use of dependent types to reason about communicating systems. I was responsible for development of a Multiparty Session Type inspired EDSL and corresponding runtime.