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.

**
The 25th edition of the Midlands Graduate School
in the Foundations of Computing Science will take place in Leicester, 8-12 April 2024.
You can find the material for the advanced course on Session Type below.
**

Office 109

School of Computer Science

Edgbaston campus

B15 2TT, Birmingham

United Kingdom

## Research

#### Journal articles

** 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.

#### Conference proceedings

** Intuitionistic Gödel-Löb logic à la Simpson: labelled systems and birelational semantics. **pdf

With Anupam Das and Iris van der Giessen. Proceedings of CSL 2024.

** A Logical Interpretation of Asynchronous Multiparty Compatibility. **pdf

With Marco Carbone and Carsten Schürmann. Proceedings of LoPSTr 2023.

** On intuitionistic diamonds (and lack thereof). **pdf

With Anupam Das. Proceedings of Tableaux 2023.

** Intuitionistic S4 is decidable. **pdf

With Marianna Girlando, Roman Kuznets, Marianela Morales and Lutz Straßburger. Proceedings of LiCS 2023. **Erratum:** Agi Kurucz noticed an oversight in the termination proof which we are currently working on patching, stay tuned for more details.

** 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.

** Focused Proof-search in the Logic of Bunched Implications. **pdf arxiv

With Alexander Gheorghiu. Proceedings of FoSSaCS 2021.

** Ecumenical modal logic. **pdf slides

With Luiz Carlos Pereira, Elaine Pimentel and Emerson Sales. Proceedings of DaLi 2020.

** Proof theory for indexed nested sequents. **pdf slides

With Lutz Straßburger. Proceedings of Tableaux 2017.

**A focused framework for emulating modal proof systems. **pdf slides

With Dale Miller and Marco Volpe. Proceedings of AIML 2016.

**Modular focused systems for intuitionistic modal logics. ** pdf slides

With Kaustuv Chaudhuri and Lutz Straßburger. Proceedings of FSCD 2016.

** Focused and Synthetic Nested Sequents. **pdf slides

With Kaustuv Chaudhuri and Lutz Straßburger. Proceedings of FoSSaCS 2016.

** Label-free Modular Systems for Classical and Intuitionistic Modal Logics. **pdf slides

With Lutz Straßburger. Proceedings of AIML 2014.

#### Selected communications

** From axioms to synthetic inference rules via focusing. **slides

Online Worldwide Seminar on Logic and Semantics - Young Researchers, 3 February 2021. **Online.**

**Fully structured proof theory for intuitionistic modal logics. **pdf

Presented by Marianela Morales at AiML 2020, Helsinki, 24-28 August 2020. **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.

**Justification logic for modal logics on an intuitionistic base. **pdf slides

Special session speaker. ASL North American annual meeting 2019. CUNY, 20-23 May 2019.

**Decomposing labelled proof theory for intuitionistic modal logic. **pdf slides

Presented at Women in Logic. Oxford, 8 July 2018.

**Nested proof systems for modal logic and beyond. **pdf slides

Presented at Twenty Years of Deep Inference. Oxford, 7 July 2018.

**Comparing BOX and ! via polarities. **pdf slides

Presented at Linear Logic: interaction, proofs and computation. Lyon, 7-10 Nov 2016.

**A cut-free proof system for pseudo-transitive modal logics. **pdf slides

Presented at TACL 2015. Ischia, 21-26 June 2015.

#### Technical reports and theses

** Forwarders as Process Compatibility, Logically. **pdf arxiv

With Marco Carbone and Carsten Schürmann. Draft.

** Synchronous Forwarders. **pdf arxiv

With Marco Carbone and Carsten Schürmann. Draft.

**Modal proof theory through a focused telescope. **hal slides

PhD thesis. Université Paris Saclay. Ecole Polytechnique. January 2018.

**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.

## Teaching

#### MGS 24 advanced course on Session Types

Material for this series of four lectures, given with Matteo Acclavio, is under construction and will be added during the school.

**Lecture 1** We start introducing the basic concepts of session types on simple processes sending/receiving messages. Lecture notes Exercise sheet

**Lecture 2** We prove some properties of the type system and introduce choice operators. Lecture notes Exercise sheet

**Lecture 3** We generalise session types to multiparty. Lecture notes Exercise sheet

**Lecture 4** We extend session types further to shared channels and recursive behaviours. Lecture notes Exercise sheet

**References**

Honda, Vasconcelos, and Kubo. Language primitives and type discipline for structured communication-based programming. ESOP 1998.

Vasconcelos. Fundamentals of session types. Information and Communication 2012.

Yoshida and Gheri. A very gentle introduction to multiparty session types. International Conference on Distributed Computing and Internet Technology 2019.

Coppo, Dezani-Ciancaglini, Padovani and Yoshida. A gentle introduction to multiparty asynchronous session types. Formal Methods for Multicore Programming 2015.

#### OPLSS 23 introductory course on Proof Theory

Material for this series of five lectures, given with Marianna Girlando, can be found at this link.

#### ESSLLI 22 advanced course on Modal Proof Theory

Material for this series of five lectures, given with Lutz Straßburger, can be found at this link.

#### At University of Birmingham

**Computer-Aided Verification.** BSc/MSci in Computer Science, 3rd and 4th year. **Fall 2022, 2023**

**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, 2023**

#### Previously

**2020/21**

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.

**2018/19**

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

**2016/17**

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.

#### MSc and BSc projects

**Logical websites**

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**

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.