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

- Ulrik Buchholtz, Floris van Doorn, Egbert Rijke.
*Higher Groups in Homotopy Type Theory*, submitted. (arXiv, Formalization (Github) - Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz.
*Homotopy Type Theory in Lean*, 8th International Conference on Interactive Theorem Proving (ITP), 2017. (arXiv, slides, Lean-HoTT library (Github), Spectral repository (Github)) - Floris van Doorn.
*Constructing the Propositional Truncation using Non-recursive HITs*, Certified Proofs and Programs (CPP), 2016. (arXiv, slides, Lean source (Github)) - Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von
Raumer.
*The Lean Theorem Prover (system description)*, International Conference on Automated Deduction (CADE-25), 2015. - Cody Roux and Floris van Doorn.
*The Structural Theory of Pure Type Systems*, Types and Lambda Calculi and Applications (TLCA), 2014. (slides) - Floris van Doorn, Herman Geuvers, Freek Wiedijk,
*Explicit Convertibility Proofs in Pure Type Systems*, Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2013. (slides, Coq formalization)

- Floris van Doorn.
*The Lean Theorem Prover*, 2 December 2015. - Floris van Doorn.
*Constructing the Propositional Truncation using Nonrecursive HITs*, 28 July 2015.

- Jeremy Avigad, Robert Y. Lewis, Floris van Doorn.
*Logic and Proof*. Lecture notes for the course Logic and Mathematical Inquiry. 2016. Interactive version. - Short notes on the
*applications of the Serre spectral sequence*, November 2015. - Floris van Doorn.
*Propositional Calculus in Coq*, arXiv:1503.08744, 9 May 2014.

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

- Formalized Spectral Sequences in Homotopy Type Theory, September 2017. Algebra, Combinatorics, and Geometry seminar, University of Pittsburgh. slides talk 1, slides talk 2
- Homotopy Type Theory in Lean, July 2017. Computer-aided mathematical proof, Cambridge. (aimed to people familiar with formalization, but not necessarily HoTT) slides video.
- The Lean HoTT library, July 2017. Big Proof, Cambridge. (aimed to people familiar with HoTT) slides video.
- On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, May 2017, prospectus defense, CMU. slides, prospectus.
- The Lean-HoTT library and the smash product, March 2017, MURI meeting at CMU. slides (slides were only for half of the talk).
- Eilenberg-MacLane spaces in Homotopy Type Theory, March 2017, ASL 2017 North American meeting. slides.
- Homotopy Type Theory in Lean, July 2016, ICMS. slides.
- Homotopy Type Theory in Lean, June 2016, HoTT/UF Workshop colocated with FSCD. slides.
- Reducing higher inductive types to quotients, May 2016, HoTT Workshop in Toronto. slides, video.
- The Lean Theorem Prover and Homotopy Type Theory (with Jeremy Avigad), May 2016, HoTT Workshop in Toronto. slides, video.
- The Lean-HoTT library and HITs in Lean, March 2016, MURI meeting at CMU. slides (slides were only for half of the talk).

- Fall 2016: TA for Differential and Integral Calculus (21-120) with Russ Walker.
- Fall 2015: TA for Logic and Mathematical Inquiry (80-211) with Jeremy Avigad. Also co-author of the lecture notes together with Jeremy Avigad and Rob Lewis.
- Spring 2015: TA for Game Theory (80-405/80-705) with Adam Bjorndahl.
- Fall 2014: TA for Formal Logic (80-310/80-610) with Steve Awodey.

- Spring 2012: TA for Discrete Mathematics with Han Hoogeveen.
- Fall 2011: TA for Foundations of Mathematics with Jaap van Oosten.