Floris van Doorn

Floris van Doorn

e-mail: fpv@andrew.cmu.edu

I am currently a third year Ph.D. student in the Philosophy Department at Carnegie Mellon University. My advisor is Jeremy Avigad and I am also working together with Steve Awodey. 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 was also trainer for the Dutch Mathematical Olympiad. Full CV (pdf).


I'm currently working on homotopy type theory, interested in higher inductive types, and working on the constrution of complicated higher inductive types using simple ones.

I'm also involved in the development of the new proof assistant Lean which is developed by Leo de Moura at Microsoft Research. I've contributed to the standard library, and I'm the main contributor of the HoTT library. I'm also the main contributor of the Spectral Sequence project, formalizing the Serre Spectral sequence in HoTT.

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


Posts on the HoTT Blog

Other work


Talks corresponding to one of my papers are listed under Publications.