Floris van Doorn

e-mail: f...@andrew.cmu.edu

I am currently a second year Ph.D. student in the Philosophy Department at Carnegie Mellon University. My advisor is Jeremy Avigad and I am enrolled in the Pure and Applied Logic program.

I previously studied at the Utrecht University in the Netherlands where I received a B.Sc. in Mathematics, a B.Sc. in Physics and a M.Sc. in Mathematics. My master thesis is Explicit convertibility proofs in Pure Type Systems supervised by Freek Wiedijk at the Radboud University Nijmegen.


I'm currently working on interactive theorem proving, working on the standard library for a new proof assistant Lean which is developed by Leo de Moura at Microsoft Research. I'm also working on the formalization of Homotopy Type Theory in Lean.

I'm interested in mathematical logic in general, and particularly in type theory, category theory, set theory and model theory.