Researcher

Bruno Gavranović

Bruno Gavranović applies category theory to deep learning, typed software and theorem proving. During his MSc at the University of Zagreb, a Haskell course helped him connect programming and mathematics; his 2019 thesis framed CycleGAN with category theory. He defended his PhD at Strathclyde in 2023, published its category-theoretic account of deep learning in 2024, and coauthored an ICML framework for neural-network architectures in 2024. He founded Coend to build neural networks that generate provably correct code. As of October 2026, he works on theorem-proving tools at Glaive, advises Google DeepMind and develops type-safe machine-learning software.

Now at
Glaive
Works
17
Citations
102
h-index
4

Publication numbers from OpenAlex, as of 19 October 2026.

Timeline

  1. 2019

    Compositional deep learning

    While studying for an MSc in computer science at the University of Zagreb, he takes a Haskell course that changes how he sees the link between programming and mathematics. A paper called Backprop as Functor introduces him to category theory. In 2019, he frames CycleGAN with a category-theoretic formalism and shows that functors can be learned with gradient descent.

  2. September 2023–2024

    A category-theoretic PhD

    At Strathclyde’s Mathematically Structured Programming Group, he defends his PhD in September 2023 with minor corrections. His 2024 thesis develops a category-theoretic mathematical foundation for deep learning.

  3. 2024

    Categorical deep learning at ICML

    At ICML 2024, he and five coauthors propose a category-theoretic framework that connects neural-network constraints with their implementations.

  4. 2025

    Building Coend

    He builds neural networks and training software for provably correct code through Coend, which he founds; he becomes Coend’s director in February 2025.

  5. January 2026

    Generalised tensors in Idris

    In January 2026, he develops Generalised Tensors as part of Glaive’s machine-learning research and implements them in TensorType using Idris.

  6. April 2026

    Types in neural networks

    In April 2026, he outlines a method for neural networks to learn output types during training and generate well-typed structures.

  7. As of October 2026

    Theorem-proving research at Glaive

    As of October 2026, he works at Glaive on a research grant to build an intermediate language for tactics and serves as a research adviser to Google DeepMind. The project develops machine-learning tactics for interactive theorem proving and a language that translates them into Lean meta-programs, supporting large language models as they create proof scripts.

Career

  1. Since 2026Glaive
  2. From 2025CoendFounder, Director

Education

  1. 2023University of StrathclydePhD
  2. University of ZagrebMSc in Computer Science

Most-cited works

  1. Categorical Foundations of Gradient-Based Learning2022 · Lecture notes in computer science · 58 citations
  2. Towards Foundations of Categorical Cybernetics2022 · Electronic Proceedings in Theoretical Computer Science · 21 citations
  3. Category Theory in Machine Learning2021 · 10 citations
  4. Compositional Deep Learning2019 · 4 citations
  5. Fibre optics2021 · 3 citations

Sources and credits

Photo: We have no published photo of Bruno Gavranović yet. Send us a free-licensed photo.

  1. About brunogavranovic.com. Checked 18 October 2026.
  2. Compositional Deep Learning arxiv.org. Checked 18 October 2026.
  3. Mathematically Structured Programming Group news msp.cis.strath.ac.uk. Checked 18 October 2026.
  4. Fundamental Components of Deep Learning: A category-theoretic approach arxiv.org. Checked 18 October 2026.
  5. Position: Categorical Deep Learning is an Algebraic Theory of All Architectures proceedings.mlr.press. Checked 18 October 2026.
  6. Bruno Gavranović brunogavranovic.com. Checked 18 October 2026.
  7. Bruno GAVRANOVIC personal appointments - Find and update company information find-and-update.company-information.service.gov.uk. Checked 18 October 2026.
  8. Generalised Tensors in Idris glaive-research.org. Checked 18 October 2026.
  9. Types and Neural Networks glaive-research.org. Checked 18 October 2026.
  10. A Structured Representation of Tactics for Machine-Assisted Theorem Proving renaissancephilanthropy.org. Checked 18 October 2026.