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

- Ulrik Buchholtz, Floris van Doorn, Jakob von Raumer.
*Homotopy Type Theory in Lean*, submitted to the 8th International Conference on Interactive Theorem Proving (ITP), 2017. (Lean-HoTT library (Github), Spectral repository (Github), arXiv) - Floris van Doorn.
*Constructing the Propositional Truncation using Non-recursive HITs*, Certified Proofs and Programs (CPP), 2016. (Lean source (Github), arXiv, slides) - 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. (Coq formalization, slides)

- 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. - Floris van Doorn.
*Propositional Calculus in Coq*, arXiv:1503.08744, 9 May 2014.

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

- On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, prospectus defense, May 2017. 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.
- The Lean Theorem Prover and Homotopy Type Theory (with Jeremy Avigad), May 2016, HoTT Workshop in Toronto. slides.
- 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.