Welcome!
Hi, I'm Adriana Baldacchino, a computer science PhD student at the University of Birmingham, supervised by Anupam Das. My main project is on proof complexity, where I'm working on developing an equational theory for monotone PV. I'm also interested in a broad range of topics, from proof theory to reverse mathematics to automata theory and graph theory.
Previously, I attained an M.Sc. in Mathematics and Foundations of Computer Science from the University of Oxford and a B.Sc. (Hons) in Mathematics and Computer Science from the University of Malta.
Most of my projects are listed below. For a detailed look at my work in and out of academia, kindly view my curriculum-vitae.
Past Projects
Master's Dissertation: Automata over Nested Data
In this work, we establish novel automata for an unboundedly nested dataset (called UNDCMA). We prove a correspondence between traces of deterministic UNDCMA with traces of a higher order language with state and control with loops, HOSC[FOSC]. This allows us to infer properties about trace approximation and reachability in HOSC[FOSC]. This is joint work with my master's supervisor Prof. Andrzej Murawski.
The correspondence with HOSC[FOSC] has been accepted at LICS. Some more results (undecidability of the projection language, a different attempt at defining automata on unboundedly nested data, extended proofs etc) can be found in my submitted thesis.
Undergraduate Dissertation: Goodstein Sequences and Unprovability of Peano Arithmetic
This was my final year dissertation for my B.Sc. at the University of Malta, and was supervised by Dr. Beatriz Zamora-Aviles. In this work, we go through the details of the proof that Goodstein's theorem is unprovable in PA. This centers mainly around three papers: Caicedo's explicit formulation of Goodstein's function in terms of fast-growing functions, Ketonen and Solovay's results on these fast-growing functions and Buchholz and Wainer's results for provably computable functions. This work involved consolidating all these results in terms of the same fast-growing functions, and giving extended proofs.
If you are interested, please find the completed work here.
Refinement Preorders for Multi-Verdict Monitors
This project was submitted as part of my B.Sc. at the University of Malta and was supervised by Prof. Adrian Francalanza. In this project, I extended my supervisor's work on monitor preorders to work for monitors which detect multiple conflicting verdicts.
The submitted work can be found here. The project is still ongoing — I have done further work in refining the monitor preorders and introducing new ones, and currently the project is in the hands of another student who is working to generalise the results to an arbitrary process language.
Colouring 2-crossing-critical graphs
This project emerged from a week-long workshop hosted by Prof. Drago Bokal from the University of Maribor at the University of Malta. This is in collaboration with Marietta Galea, Prof. Drago Bokal and Prof. John Baptist Galea. In this work, we close the open problem of chromatic numbers of arbitrary large 2-crossing-critical graphs by providing an explicit characterisation.
Some slides presenting our results can be found here.
CERN Summer Student Project
As part of my Summer student experience at CERN in the Summer of 2023, I embarked on a project with the IT department on integrating Overleaf support with CERNBox, the storage software used at CERN. This project was supervised by Javier Ferrer and Giuseppe Lo Presti.
My report on this project can be found online at this link.
All content, unless otherwise stated, on this site is © Adriana Baldacchino (2026).