Categorical Semantics and Verification of Reactive Programs
This PhD project will aim for a categorical semantics and program logics of reactive programs. Categorical structures are well-suited as semantics of programs with generic effects: they allow precise tailoring of the axioms to specific classes of programs, and provide the necessary abstraction and compositionality that ease human understanding.
Reactive programs take infinite streams of inputs and produce infinite streams of outputs [1]. Such programs express models or specifications of machines that run indefinitely: machines that receive inputs from the environment and produce outputs accordingly. The outputs of these machines are not assumed to depend functionally on the inputs, so that programs may express probabilistic models, such as partially observable Markov decision processes [6], or allow other kinds of program effects, such as nondeterminism and access to a global state.
Possible concrete sub projects:
Categorical structure of reactive programs. Effectful streams give categorical semantics to effectful reactive programs, but only consider their data flow [3,5]. This project would aim at increasing the expressivity of the reactive programs that we can give semantics to. The categorical structure should be able to express the control flow of programs to give semantics to program statements like if-else choices and while loops. Semantics of higher-order computations would also require additional categorical structure.
Program logics for reactive programs. Categorical semantics informs the development of appropriate program logics: for imperative programs, the rules of Hoare-like logics derive from the categorical structure of their denotational semantics [2]. This project would aim at finding an appropriate categorical structure, building on the previous project, that derives rules for verification of reactive programs. In particular, the internal logic of predicates that is determined by the categorical structure should be able to express temporal properties of programs.
Quantitative program logics and approximate traces via metric enrichment. Quantitative reasoning is more appropriate when dealing with probabilistic programs: their behaviour may not be exactly the same, but it may be the same with very high probability [4]. This project would aim at adding quantitative aspects to both the semantics and the program logic of reactive programs. A technique that may help achieving this is metric enrichment.
Responsibilities:
- Research in categorical methods for computer science.
- Publish results in international peer-reviewed conferences and journals.
- 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.
- Ability to write mathematical proofs.
- Some knowledge of category theory.
- English communication skills.
The following experience is beneficial:
- Good knowledge of category theory.
- Background and interest in Theoretical Computer Science
References:
[1] Engineer Bainomugisha, Andoni Lombide Carreton, Tom van Cutsem, Stijn Mostinckx, and Wolfgang de Meuter. A survey on reactive programming. ACM Computing Surveys, 45(4), August 2013. doi:10.1145/2501654.2501666.
[2] Filippo Bonchi, Alessandro Di Giorgio, and Elena Di Lavore. A diagrammatic algebra for program logics. In Parosh Aziz Abdulla and Delia Kesner, editors, Foundations of Software Science and Computation Structures, pages 308–330. Springer Nature Switzerland, 2025. doi: 10.1007/978-3-031-90897-2_15.
[3] Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful mealy machines: Bisimulation and trace. In Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2025), pages 541–554, 2025. doi:10.1109/LICS65433.2025.00047.
[4] Josée Desharnais and Ana Sokolova. ϵ-Distance via Lévy-Prokhorov Lifting. In Stefano Guerrini and Barbara König, editors, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026), volume 363 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:24, Dagstuhl, Germany, 2026. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.26, doi:10.4230/LIPIcs.CSL.2026.26.
[5] Elena Di Lavore, Giovanni de Felice, and Mario Román. Monoidal Streams for Dataflow Programming. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022), pages 1–14, 2022. arXiv:2202.02061, doi:10.1145/3531130.3533365.
[6] Joost-Pieter Katoen. The probabilistic model checking landscape. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), page 31–45, New York, NY, USA, 2016. Association for Computing Machinery. doi:10.1145/2933575.2934574.
Supervisors:
Main supervisor: Researcher Elena Di Lavore: 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: Department of Software Science: Laboratory for Compositional Systems and Methods
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 ambition of the Department of Software Science is to be a leading actor in software science research in the Baltic Sea region and an intermediary of top level and scientifically relevant competence between students, enterprises, public sector and researchers.
For information about the admission process, please visit the PhD Admission homepage
Applications can be submitted from 01.06.2026 to 30.06.2026
