Dr Jan de Muijnck-Hughes

Lecturer

Computer and Information Sciences

Personal statement

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.

Publications

Back to staff profile

Publications

Colouring flags with Dafny & Idris: de Muijnck-Hughes Jan, Noble James; Dafny 2024 (2024)
Capable : a mechanised imperative language with native multiparty session types: Muijnck-Hughes Jan de, Urlea Cristian, Voinea Laura, Vanderbauwhede Wim; ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (2023)
Wiring circuits is easy as 0, 1, omega, or is it... (Artifact): Muijnck-Hughes Jan de, Vanderbauwhede Wim; , pp. 4:1-4:3 (2023); https://doi.org/10.4230/DARTS.9.2.4
Wiring circuits is easy as {0,1,w}, or is it...: de Muijnck-Hughes Jan, Vanderbauwhede Wim; 37th European Conference on Object-Oriented Programming, ECOOP 2023 37th European Conference on Object-Oriented Programming, ECOOP 2023 Leibniz International Proceedings in Informatics, LIPIcs Vol 263 (2023); https://doi.org/10.4230/LIPIcs.ECOOP.2023.8
Type theory as a language workbench: de Muijnck-Hughes Jan, Allais Guillaume, Brady Edwin; Eelco Visser Commemorative Symposium (EVCS 2023) Open Access Series in Informatics (OASIcs) Vol 109 (2023); https://doi.org/10.4230/OASIcs.EVCS.2023.9
A framework for resource dependent EDSLs in a dependently typed language: de Muijnck-Hughes Jan, Brady Edwin, Vanderbauwhede Wim; 34th European Conference on Object-Oriented Programming, ECOOP 2020 34th European Conference on Object-Oriented Programming, ECOOP 2020 Leibniz International Proceedings in Informatics, LIPIcs Vol 166 (2020); https://doi.org/10.4230/LIPIcs.ECOOP.2020.20

More publications

Teaching

Back to staff profile

Teaching

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)

Research

Back to staff profile

Research Interests

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!