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.
Timeline
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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
- Since 2026Glaive
- From 2025CoendFounder, Director
Education
- 2023University of StrathclydePhD
- University of ZagrebMSc in Computer Science
Most-cited works
Sources and credits
Photo: We have no published photo of Bruno Gavranović yet. Send us a free-licensed photo.
- About
- Compositional Deep Learning
- Mathematically Structured Programming Group news
- Fundamental Components of Deep Learning: A category-theoretic approach
- Position: Categorical Deep Learning is an Algebraic Theory of All Architectures
- Bruno Gavranović
- Bruno GAVRANOVIC personal appointments - Find and update company information
- Generalised Tensors in Idris
- Types and Neural Networks
- A Structured Representation of Tactics for Machine-Assisted Theorem Proving