Dr Maximilian Doré

I’m working on computer proof assistants, which are tools that help in the construction and verification of mathematical proofs. My main goal is to help bring these tools into the mathematical practice, both by working on logical foundations and applications. I am primarily working with Cubical Agda, which is a proof assistant particularly suited to reasoning about abstract topology. Current projects include using Cubical Agda to formalise topological data analysis; and proof synthesis in Cubical Agda.

I teach a variety of introductory CS courses at Merton, primarily on the theoretical and algorithmic side. These include Functional Programming, Models of Computation and Algorithms and Data Structures. The aim of these courses is to teach students about syntax, computability and complexity of algorithms before they specialise in their third and fourth years. 

Recent publications:

M. Doré, E. Cavallo and A. Mörtberg, Automating Boundary Filling in Cubical Agda, arXiv:2402.12169