Maximilian Doré
I'm Departmental Lecturer in Computer Science at the University of Oxford, as well as College Lecturer at Somerville and Merton College. I'm interested in dependent type theory, both as a programming language and as a logic for the formalisation of mathematics.
I did my DPhil under the supervision of Samson Abramsky and Sam Staton. Before coming to Oxford, I studied at RWTH Aachen, Imperial College London and LMU Munich.
If you want to work with me; do a student project; or just want to chat about something please get in touch! I'm always interested to explore new topics in programming languages, interactive/automated theorem proving, and logic in general.
Publications
| preprint |
Dependent Multiplicities in Dependent Linear Type Theory
arXiv:2507.08759
GitHub:maxdore/dltt/
|
| ICFP 2025 |
Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl) 30th ACM SIGPLAN International Conference on Functional Programming
doi:10.1145/3747531
(Open Access)
GitHub:maxdore/dynltt/
|
| TYPES 2025 |
Linear Types inside Dependent Type Theory (Extended Abstract) 31st International Conference on Types for Proofs and Programs |
| AITP 2024 |
Forward Reasoning in Hindsight (Project Proposal) with Michael Rawson, Zsolt Zombori and Christoph Wernhard 9th Conference on Artificial Intelligence and Theorem Proving |
| FSCD 2024 |
Automating Boundary Filling in Cubical Agda with Evan Cavallo and Anders Mörtberg 9th International Conference on Formal Structures for Computation and Deduction
doi:10.4230/LIPIcs.FSCD.2024.22
(Open Access)
GitHub:maxdore/dedekind/
|
| ThEDU 2019 |
Towards Intuitive Reasoning in Axiomatic Geometry with Krysia Broda 7th International Workshop on Theorem proving components for Educational software
doi:10.4204/EPTCS.290.4
(Open Access)
|
| CSEDU 2019 |
Intuitive Reasoning in Formalized Mathematics with ELFE with Krysia Broda 10th International Conference on Computer Supported Education |
Recent Talks
| 28/08/2025 |
Using generative AI in theoretical computer science
(invited)
AI Transforms Math Research Workshop University of Augsburg |
| 13/06/2025 |
Linear Types inside Dependent Type Theory
31st International Conference on Types for Proofs and Programs (TYPES) Strathclyde University Glasgow |
| 17/04/2025 |
Linear Types with Dynamic Multiplicities in Dependent Type Theory
EuroProofNet WG6 Meeting on syntax and semantics of type theory University of Genoa |
| 10/10/2024 |
Reasoning with Kan fillings about Morse reductions
(invited)
Seminar on Formalisation of mathematics with interactive theorem provers Cambridge University |
| 08/08/2024 |
Formalising Topological Data Analysis in Cubical Agda
(invited)
DANGER 4: Data, Numbers and Geometry London Institute for Mathematical Sciences |
| 28/06/2024 |
Automating Reasoning in Cubical Type Theory
Prospects of Formal Mathematics, Trimester Program Hausdorff Center for Mathematics, University of Bonn |
| 13/03/2024 |
(Automatically) verifying Morse reductions in Cubical Agda
Proglog meeting Chalmers University Gothenburg |
Theses
| 2023 |
Computing Spaces in Type Theory DPhil Computer Science, University of Oxford, Wolfson College doi:10.5287/ora-9roxkxozq |
| 2019 |
Constructivity in Homotopy Type Theory MA Logic and Philosophy of Science, LMU Munich PDF download |
| 2018 |
ELFE – An interactive theorem prover for undergraduate students BSc Computer Science, RWTH Aachen (BEng Individual Project at Imperial College) PDF download |