Floris van Doorn

Floris van Doorn

e-mail: fpvdoorn@gmail.com

Starting fall 2018 I am going to work with Tom Hales on the formal abstracts projects at the mathematics department of the University of Pittsburgh.

Until summer 2018 I was a Ph.D. student at Carnegie Mellon University under supervision of Jeremy Avigad and Steve Awodey. My dissertation was titled On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory.

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).

Research

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.

Dissertation

My dissertation was titled On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory and was supervised by my dissertation committee: Jeremy Avigad, Steve Awodey, Ulrik Buchholtz and Mike Shulman.

Publications

Posts on the HoTT Blog

Other work

Selected Talks

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

Teaching

CMU UU