CoLab Logo

Team

Dr Ornela Dardha - Team Lead

Photo of Ornela Dardha

I am a Senior Lecturer (Associate Professor) in the School of Computing Science at the University of Glasgow. Within the School, I am the Theme Lead of Programming Languages and a member of Formal Analysis, Theory and Algorithms (FATA). I am Glasgow Site Leader of the European RISE Action Behavioural Application Program Interfaces (BehAPI) and previously I was a Co-I and a Postdoctoral Researcher of the UK EPSRC programme grant From Data Types to Session Types: A Basis for Concurrency and Distribution (ABCD). My research interests are in programming languages, concurrency, logic and verification. My goal is to design and develop rigorous formal models and software tools for communication-safe, adaptable and resilient concurrent and distributed systems.

Matthew Alan Le Brun

I started my PhD with the School of Computing Science at the University of Glasgow in January 2022, under the supervision of Dr Ornela Dardha and Dr Simon Fowler. I have previously completed a BSc and MSc in Computing Science at the University of Malta, where I focused on distributed computing, fault-tolerance, and consensus. My research has now shifted to session types for distributed computing protocols, with a specific focus on consensus algorithms.

Photo of Matthew Alan Le Brun

Arwa Hameed Alsubhi

Photo of Arwa Hameed Alsubhi

I completed my MSc in Computing Science, at the University of Glasgow in 2022. During my MSc, I started developing the Coconut tool with Dr Ornela Dardha, which is a typestate-based library for C++ language that allows to define and enforce protocols for C++ objects. I started my PhD in October 2022 under the supervision of Dr Ornela Dardha. I will be working to investigate approaches, both theoretically and practically, to create sound, effective and scalable interoperable typestate-based tools.

Ivan Nikitin

I am a PhD student at the University of Glasgow under the supervision of Dr Colin Perkins and Dr Ornela Dardha. I focus on using formal methods to improve network protocol specifications and the network protocol standardisation process. Before this, I completed my undergraduate at UofG in June 2022, with my final year dissertation analysing QUIC as a transport layer for IoT devices, specifically as the transport layer for the MQTT protocol.

A picture of Ivan

Past Members

Photo of Uma Zalakain
Uma Zalakain

Now in industry

Photo of Mathias Jakobsen
Mathias Jakobsen

Now in industry

Photo of Luke Gall
Luke Gall

MSci graduate / Now in industry

Awards

Award Title Awarded To Awarded By
Science, She Says! Award Ornela Dardha Italian Ministry of Foreign Affairs and International Cooperation (2023)
PPDP 10 Year Most Influential Paper Award Ornela Dardha ACM's PPDP Steering Committee (2022)
MSci Class Prize 2021-22 for the most outstanding single honours student in Computing Science Luke Gall School of Computing Science (2022)
Best Italian PhD Thesis in Theoretical Computer Science 2015 Ornela Dardha Italian Chapter of EATCS (2015)

Papers

Title Venue Authors Links
MAGπ: Types for Failure-Prone Communication (Extended Abstract) PLACES 2023 Matthew Alan Le Brun, Ornela Dardha
MAGπ: Types for Failure-Prone Communication ESOP 2023 Matthew Alan Le Brun, Ornela Dardha
Coconut: Typestates for C++ (Extended Abstract) PLACES 2022 Arwa Alsubhi, Ornela Dardha
Capable GV: Capabilities for Session Types in GV (Extended Abstract) PLACES 2022 Magdalena Latifa, Ornela Dardha
Co-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract) TyDe 2021 Uma Zalakain, Ornela Dardha
Papaya: Global Typestate Analysis of Aliased Objects PPDP 2021 Mathias Jakobsen, Alice Ravier, Ornela Dardha
π with Leftovers: A Mechanisation in Agda FORTE 2021 Uma Zalakain, Ornela Dardha

Tools

Papaya is an implementation for Scala of global typestate analysis allowing unrestricted aliasing. It is implemented as a compiler library for Scala, allowing it to be embedded into real-life programs, verifying at compile time that protocols are being adhered to by all instances. The protocols are expressed as singleton classes and thus are written in Scala itself. Using the @Typestate annotation a protocol is linked to a class, and the tool will generate errors or warning if instances of this class do not respect the protocol, or if a protocol is potentially left unfinished.
Coconut introduces typestates in C++ through a typestate-based library, providing templates for protocol definitions. Objects can then be statically checked against these protocols to ensure they behave accordingly. This project is expected to aid programmers by helping them detect violations of protocols that they themselves define, making the programming process more flexible, practical, and trouble-free.
Timed Mungo is an extension to the Mungo toolchain, that adds a timed variant of typestates to Java programs. Using the extended StMungo tool a timed multiparty session type is projected into local protocols which, using the @Typestate annotation, can be added to a Java class. Timed Mungo will then verify that the protocol is adhered to, within the specified timing constraints.
Tropicode is a tool for analysing typestates for languages targeting the Java Virtual Machine (JVM). As opposed to the previous tool, Tropicode works on the compiled low-level JVM bytecode, making it possible to check protocols in all languages targeting the JVM such as Java, Kotling, and Clojure. Out of the box it provides a Java integration with a @Protocol annotation that can be added directly to classes. It also provides mechanisms to add protocol to pre-existing classes such as the Java standard library.

Outreach Activities

Glasgow Science Festival 2023

CoLab had the privilege of hosting a booth titled "How Computers Talk" at the annual Glasgow Science Festival held at the Riverside Museum. Our aim was to introduce young children to the fascinating world of communication protocols through two exciting games: a treasure hunt tabletop game and a motorbike assembly game. Working collaboratively, young children eagerly devised protocols to assist our adventurous pirate in reaching the treasure. Along the way, they gained valuable insights into the concept of sequence charts and even had the opportunity to construct a motorbike using message sequences. Participating in the Glasgow Science Festival and being able to inspire and ignite young children’s curiosity in the field of computing science was a wonderful experience.

Glasgow Science Festival 2022

Twice during the annual Glasgow Science Festival, CoLab hosted a stand at the Riverside Museum, introducing the concept of communication protocols through a treasure hunt tabletop game. The primary audience was young children, and while the chocolatey prize helped to grab their attention, it was great to see them engage and have fun while working together to devise a protocol that would help our pirate reach the treasure. It was a rewarding experience to have the chance to inspire young people to pursue computing science.

CoLab members wearing Glasgow Science Festival T-shirts
CoLab members wearing CoLab T-shirts

π