Categorical Logic and Semantics of Message Passing
The PhD project will explore the application of category theory—specifically, of duoidal categories and its variants—to the semantics of message passing: one of the paradigms in concurrent programming. This project explicitly targets a theory of duoidal concurrent message passing; the project aims to develop a universal model of concurrency on top of a symmetric monoidal category.
The project will address the following key areas:
Symmetric monoidal categories are successful at process description: they provide an intuitive syntax and an expressive algebra for processes. Models of symmetric monoidal categories include non-deterministic processes, Markov kernels, effectful computations, quantum programs, or computable functions. Still, they are insufficient for the task of describing concurrency: if monoidal categories capture the essential algebra of processes, we are missing the essential algebra of concurrent processes.
A commonly overlooked angle is that of duoidal categories and its variants. For instance, the internal logic of a physical polarized monoidal multicategory translates, in a Curry-Howard isomorphism, to the types for sequential message passing. Moreover, there exists an adjunction between the algebras of a physical polarized monoidal multicategory—message theories—and symmetric monoidal categories—process theories. While encouraging, it is still a preliminary result that leads to multiple research avenues.
This project will address the following research questions:
- What is a Curry-Howard correspondence for truly concurrent message passing processes? What is their internal logic? What is a combinatorial characterization of the free such algebra?
- What is a semantics and an intuitive syntax for concurrent choice and iteration?
- Can we develop metalanguages for effectful message passing? What is their categorical semantics? What is an interpreter for these metalanguages?
- Can we develop causality and contextual equivalence within this framework?
Responsibilities and (foreseen) tasks:
- Research in categorical semantics and categorical methods for computer science.
- Advance categorical logic. In particular, advance the logic of concurrent processes.
- Develop syntax and domain-specific languages based on categorical structures.
- Prepare and publish articles in international peer-reviewed venues.
- Contribute to the intellectual environment in the Compositional Systems and Methods group at TalTech by giving seminars, actively contributing to reading groups, etc.
Applicants should fulfil the following requirements:
- An MSc degree in Mathematics, Computer Science, or related subjects.
- A basic knowledge of category theory.
- Ability to write mathematical proofs, and to express formal ideas clearly.
- English verbal and written communication skills.
The following experience is beneficial:
- Experience with functional programming or proof assistants.
- Interest in categorical logic and categorical syntax.
- A broad knowledge of category theory.
- Ability to work independently and as part of a research group.
Supervisors:
Main supervisor: Researcher Mario Román García: School of Information Technologies: Department of Software Science: Laboratory for Compositional Systems and Methods
Co-Supervisor: Tenured Full Professor Pawel Maria Sobocinski: School of Information Technologies: Dean's Office at School of Information Technologies
Tallinn University of Technology (TalTech) is an international scientific community with approximately 9,000 students and 2,000 employees; it is one of the largest universities in Estonia, the leading EU country in digitalisation. The university's strengths are broad multidisciplinary study/research interests, a modern research environment, and strong collaboration with international educational and research institutions. TalTech is aiming to be an organisation leading the way to a sustainable digital future.
The mission of the Department of Software Science is to advance internationally and nationally relevant state of the art in research and apply it in bachelor, MSc and doctoral education in the areas of computer science, information systems, data science, artificial intelligence and cyber security with the goal to solve problems the society is facing and support sustainable development.
The purpose of the research groups at the Department of Software Science is to advance internationally and nationally relevant state of the art in research in the areas of computer science, information systems, data science, artificial intelligence and cyber defence. The research groups and laboratories are autonomous, strong and successful participants in attracting research funding and are able and willing to participate in research and innovation heavy collaboration with enterprises and the public sector, both in Estonia and abroad.
For information about the admission process, please visit the PhD Admission homepage
Applications can be submitted from 12.06.2026 to 12.07.2026
