UniCaToR
Starting from the 1st of September, 2026 I am working on my CTU Starting grant UniCaToR, which stands for A Unification of Categorical Theories of Resources.
I am hiring a postdoc and a PhD student:
- Topics:
- category theory (theory of comonads, categorical semantics)
- linear type theory/logic
- programming language theory
- The group structure:
- the postdoc will work closely with the PI (Tomáš Jakl) to develop the foundations of the theory
- the PhD student is tasked to focus on the implementation side of things (in Haskell/OCaml/Lean/…), however, won’t be discouraged from focusing on the theory too
- small budget is allocated for master students to develop examples
- Postdoc duration: 1-2 years (based on common agreement)
- PhD funding is for up to 4 years
- The positions include some travel money to attend approximately 3 conferences/workshops per year
- Salaries are competitive (ask!).
- Deadline for applications: 31 September 2026
- Write to me if you are interested!
- IMPORTANT:
- Postdoc applicants are highly encouraged to first apply for the CROP Postdoctoral Fellowship (deadline 31 August 2026!). If succesful, this will allow our team to grow even bigger!
A brief description of this project:
The aim of this project is to develop a mathematical theory suitable for reasoning about programming language resources. This will serve as a basis for a mathematically rigorous type system which, in turn, will allow a compiler implementing this type theory to check specified resource usage guarantees. Similar theories of such kind have existed in the past (e.g. the theory of coeffects) and, also, the industry has shown us that programming languages with resource usage guarantees are on demand (e.g. Rust and its memory safety guarantees).
Our approach aims to extend the theory of comonads, which is a fundamental concept from the field of pure mathematics called category theory. Comonads offering similar resource control also exist outside of Rust (e.g., to ensure correct CPU usage or protecting sensitive data) but, despite their usefulness, their study remains scattered, with each resource type typically studied in isolation. Therefore, the principal goal of this project is to unify the study of computational resources by developing a theory of presentations of comonads. By ‘presentations’, we mean a mathematical language for specifying comonads. Currently, only ad-hoc methods exist for constructing new comonads, which drastically limits their flexibility. A common language will allow us to compare and combine different uses of comonads, derive their properties, and transfer techniques across theoretical computer science. Progress on the theoretical side will also enable practical advancements. It will pave the way for automated reasoning tools about program resources, new language constructs, and better correctness guarantees of resource usage. For example, it could enable an extension of a type system to provide running-time and memory access count guarantees. To stress-test our framework, we will implement a prototype programming language (in Haskell/OCaml/Lean/…) with custom resource constraints, checked at compile-time.
Project activity
- 9 August 2026: call for a postdoc and PhD opened
Acknowledgement
The project is funded by the generous support of the Czech Technical University and the Faculty of Information Technology.