Maximilian Doré

Dr Maximilian Doré
Room
415,
Wolfson Building,
Parks Road, Oxford OX1 3QD
United Kingdom
Themes:
Interests
My main research interest is type theory, which connects logic with programming. Type theories can be used to encode a program's behaviour in a programming language, but also to formalise contemporary mathematics. I want to further understand foundational problems in the area of type theory, as well as utilise its power in more applications.
As a departmental lecturer I'm lecturing Lambda Calculus and Types and run practicals for several courses, most of them are about different programming language paradigms. I'm also a college lecturer at Somerville and Merton, where I tutor a variety of courses.
If you want to work with me, or do a student project, please get in touch! I'm always interested to explore new topics in interactive/automated theorem proving, programming languages, and logic in general.
Recent publications
2025, Dependent Multiplicities in Dependent Linear Type Theory, preprint arXiv:2507.08759
[preprint] [code]
2025, Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl), International Conference on Functional Programming (ICFP)
[preprint] [code]
2024, Automating Boundary Filling in Cubical Agda, with Evan Cavallo and Anders Mörtberg, 9th International Conference on Formal Structures for Computation and Deduction (FSCD)
[paper] [code]
Biography
I did my DPhil in Oxford under the supervision of Samson Abramsky and Sam Staton. Before coming to Oxford, I completed a master's in Logic and Philosophy of Science at the MCMP at LMU Munich. In my master's thesis, I tried to give philosophical underpinning to why a classical mathematician should embrace constructive reasoning and, conversely, why a type theorist can have peace of mind being a realist about mathematics. And before that, I did a bachelor's in Computer Science and Mathematics at RWTH Aachen. I spent the last year of my bachelor's at Imperial College London, where I worked with Krysia Broda on the Elfe prover.