Floris van Doorn

Floris van Doorn

e-mail: fpv@andrew.cmu.edu

I am currently a 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 am working on homotopy type theory, which is a connection between homotopy theory and type theory. My main interest here in this field is synthetic homotopy theory, which is the study of types as spaces in algebraic topology. Since the homotopy theoretic definitions are very close to the logical foundations, it is feasible to formalize complicated results in a proof assistant.

I have done this in 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 am also the main contributor of the Spectral Sequence project, where we have formalized the (cohomological) Serre and Atiyah-Hirzebruch spectral sequences. We are currently working on porting the results to Lean 3.

Another topic in Homotopy type theory I am interested in is higher inductive types, trying to construct complicated higher inductive types from simple ones.

I am also interested in mathematical logic. I have worked more on type theory and category theory and I'm fascinated by forcing in set theory.


Posts on the HoTT Blog

Other work


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