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 mainly tasked to focus on the implementation side of things, however, won’t be discouraged from focusing on the theory too
- small budget is 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:
Recently, the Rust programming language has seen massive industry adoption because of its memory safety guarantees and a high level of abstraction while retaining the speed of low-level languages. These guarantees stem from its mathematically rigorous type system, which allows the compiler to reject programs with fundamental logical flaws. This rigorous theory relies on comonads—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 main 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 Rust’s type system to provide running-time and memory access count guarantees. To stress-test our framework, we will implement a prototype programming language 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 Sciences.