I am a Lecturer in the Department of Computer and Information Sciences and a member of StrathCyber and the Mathematically Structured Programming groups.

In Welsh English the word ‘tidy’ describes anything that is positive, good, neat.... How we engineer our software is not tidy, I want to change that!

My research investigates making system engineering more trustworthy by making it more TyDe: Type-Driven.

TyDe techniques explore applications of cutting-edge programming language theory to fundamentally change the way we engineer systems by interlinking our System's specifications and implementations. To do so, I investigate novel combinations of type systems, dependent types, & functional programming. With this TyDe approach, we can: reduce mismatches between a system’s specification and implementation; increase productivity of system creation and verification; and fundamentally enhance system trustworthiness. TyDe techniques benefit both Society and the Economy by guaranteeing that our systems are trustworthy because our engineering practises are also trustworthy!

Please see my personal website for more information.

Generally speaking, my research interests involve making Systems Engineering more TyDe: Type-Driven. I want to combine cutting-edge programming language theory (namely novel combinations of 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.

Functional programming is a well studied domain for describing how we can structure our code and specifications. I have used functional programming as the foundation in which to specify novel encodings of hardware interface specifications and the languages themselves.

Type Systems enable us to describe what it means for a program and specification to be correct. I have used novel typing disciplines to encapsulate good structure of hardware designs and also the behaviour of programs.
I have also explored the use of behavioural types and resource-aware type systems to ensure that existing programs behave correctly by retrofitting their design with a new type system.

Dependent types are an expressive environment in which we can reason about, and realise, our software, leveraging the Curry-Howard correspondence that our programs are proofs when our types are propositions.
I have long used the Idris programming language to mechanise my results and explore how best to use dependent types to structure our programs. I have begun exploring how we can use dependent types to provide machine executable language specifications.

There are more topics (privacy and cryptography) that I am interested in, but the above keeps me busy for now!

I teach on topics relating to functional programming, formal verification, and Cyber Security. Specifically, I teach on the following Masters level modules:

• CS813: Advanced Information Security
• CS886: Advanced Security-by-Design

I also supervise undergraduate and masters projects. Specifically, I supervise students taking:

• CS408 Individual Project (BSc (Hons) Final Year Dissertation)
• CS958 Individual Project (MSc Dissertation Project)
• CS811 Dissertation  (MSc GA Cyber Dissertation Project)