Provably correct efficient tensor processing and containers

Tensor processing is central in machine learning and quantum computation. Containers are a formalism from functional programming and type theory for representing a wide variety of types of datastructures and transformations between them. The objective of this PhD project is to advance the theory of containers and its experimental implementations to address challenges in provably correct efficient tensor processing.

The project will address the following key areas:

Tensors are a representation of multilinear maps, a multidimensional version of matrices. Tensor processing is central in machine learning and quantum computation. There are dedicated libraries for tensor programming targeting GPUs and specialized hardware such as TensorFlow, PyTorch and JAX, also some frameworks that provide guarantees of correctness like ATL. Data movement is a costly bottleneck to full utilization of the operation parallelism offered by hardware.

Containers are a formalism from functional programming and type theory for representing a wide variety of types of datastructures and transformations between them. Some researchers, notably Šinkarovs and Gavranovic with colleagues, have experimented with applying containers to tensor programming.

The objective in this PhD project is to advance the theory of containers and its experimental implementations to address challenges in provably correct efficient tensor processing. This will cover variations of containers dealing with eg algebraic structure on data and datastructures (eg commutative monoids, semirings), explicit representation of and reasoning about data layouts and movement.

Responsibilities and (foreseen) tasks:

• The student’s primary responsibility is research on this PhD project.
• The student may have contribute to the teaching activities of the lab as a course assistant.

Applicants should fulfil the following requirements:

• The candidate must have an MSc degree in computer science or mathematics.
• The successful candidate is knowledgeable in at least a couple and interested in all of the following: linear algebra, functional programming, computer architecture, type theory, category theory, program analysis, certified programming.

The following experience is beneficial:

• The successful candidate must be a good programmer.

Supervisors:

Main supervisor: Leading Researcher Tarmo Uustalu, School of Information Technologies: Department of Software Science:

Co-Supervisor: Lecturer Philipp Joram, School of Information Technologies: Department of Software Science:

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 Department of Software Science is a leading computer science department in Estonia. In particular, we are strong in programming language theory, logic, type theory, category theory. The relevant labs are the High-Assurance Software Laboratory, incl the Logic and Semantics Group, and the Lab for Compositional Systems and Methods. We have a number of PhD students working in these domains, we collaborate with many European centers, receive many visitors.

For information about the admission process, please visit the PhD Admission homepage

Applications can be submitted from 26.08.2026 to 26.09.2026