I am a lecturer in the School of Computer Science at the University of Birmingham.
I am part of the Theory of Computation research theme.
I am interested in supervising MSc and BSc students projects. See list of ideas below.
Until October 2021, I was a research fellow at University College London in the PPLV team. I worked on the ReLiC project with David Pym and Alexandra Silva.
Until September 2019, I was a postdoctoral researcher at IT-University in the Meta-CLF2 project, led in Copenhagen by Carsten Schürmann.
I obtained my Ph.D. in January 2018, at Inria Saclay under the supervision of Lutz Straßburger and Dale Miller.
School of Computer Science
B15 2TT, Birmingham
From axioms to synthetic inference rules via focusing. pdf
With Dale Miller, Elaine Pimentel and Marco Volpe. Annals of Pure and Applied Logic. May 2022.
Justification logic for constructive modal logic. pdf hal
With Roman Kuznets and Lutz Straßburger. Special Issue of the Journal of Applied Logics on Intuitionistic Modal Logic and Applications. September 2021.
A fully labelled proof system for intuitionistic modal logics. pdf hal
With Marianela Morales and Lutz Straßburger. Special Issue of the Journal of Logic and Computation on External and Internal Calculi for Non Classical Logics. May 2021.
Modal logic and the polynomial hierarchy: from QBFs to K and back. pdf
With Anupam Das. Proceedings of AiML 2022.
A pure view of ecumenical modalities. pdf
With Luiz Carlos Pereira, Elaine Pimentel and Emerson Sales. Proceedings of WoLLIC 2021.
From axioms to synthetic inference rules via focusing. slides
Online Worldwide Seminar on Logic and Semantics - Young Researchers, 3 February 2021. Online.
Intuitionistic modal proof theory: something old, something new. pdf
Special session speaker. ASL North American annual meeting 2020. UC Irvine, 25-28 March 2020. Cancelled!
Formalising concurrent computation: CLF, Celf, and applications.
Tutorial speaker. Tableaux 2019. Middlesex University, London, 3-5 September 2019.
Technical reports and theses
On the proof theory of indexed nested sequents for classical and intuitionistic modal logics. hal
With Lutz Straßburger. Inria. April 2017.
Focused and Synthetic Nested Sequents. (Extended Technical Report) hal
With Kaustuv Chaudhuri and Lutz Straßburger. Inria. January 2016.
MSc and BSc projects
It can be useful for learners and practitioners alike to have access to websites that let you explore certain logical systems, sytactically or semantically.
Syntax There are interactive web interfaces for deriving valid formulas in first order logic and in linear logic.
Semantics The modal logic playground is a great way to visualize Kripke models. It has also been extended to dynamic epistemic logic.
Logic and Machine Learning
ML applied to Logic ML techniques can be applied to logical problems, such as to improve current automated reasoning techniques.
Logic applied to ML Vice-versa to increase precision of learning algorithms, they can be combined with logical models. For example, composing neural learning and symbolic reasoning.
Learning logic, maths, and theories of computation.
In the first years of your Computer Science degree, you had to wrestle with learning some mathematical and logical foundations of CS as well as some of the theory of computation (e.g. finite automata, Turing machines). How could you make this easier for the next generation of students? Why not develop some game-based learning applications?
Logic for communicating processes
In the two papers on forwarders above, we refined the logical description of communicationg processes and design a sort of forwarder logic. An implementation of this system could allow us to decide whether a set of agents are able to communicate or not.
Theorem provers take a theoretical system into a practical way to decide the validity of a statement in a given logic. For example, the logical systems for normal modal logics based on nested sequents and on labelled sequents have been turned into theorem provers called MOIN and MOILab. Similarly with PRONOM for non-normal modal logics.
Logic for social phenomena
Modal logics are a way to extend the expressivity of propositional logic beyond true or false statements. One interpretation of modalities is given by epistemic logic, a way to represent the epistemic state/behaviour of one or many agents such as knowledge or beliefs. Recent examples are a logic to reason about social influence or about visibility in social networks.
At University of Birmingham
Computer-Aided Verification. BSc/MSci in Computer Science, 3rd and 4th year. Fall 2022
Theories of Computation. BSc in Computer Science, 1st year. Spring 2022, 2023
Mathematical and Logical Foundations of CS. BSc in Computer Science, 1st year. Fall 2021
Teaching Assistant. Theory of Computation. UCL, London. BSc in Computer Science, 1st year.
Teaching Assistant. Directed Reading. UCL, London. MEng in Mathematical Computation, 2nd year.
Teaching Assistant. Logic. UCL, London. BSc in Computer Science, 2nd year.
Co-lecturer. Linear algebra and probability. IT-University, Copenhagen. MSc in IT, Computer Science.
Teaching Assistant. Machine learning. IT-University, Copenhagen. BSc in Data Science, 2nd year.
Guest lecturer. Cognitive psychology. Carnegie Mellon University Qatar. slides
Teaching assistant. Integration and linear algebra. UPMC, Paris. BSc in Mathematics, 1st year.
Teaching assistant. Multiple variables and vectorial analysis. UPMC, Paris. BSc in Mathematics, 2nd year.