Explicit convertibility proofs in pure type systems. - Floris van Doorn; Herman Geuvers; Freek Wiedijk (LFMTP, 2013)

The Structural Theory of Pure Type Systems. - Cody Roux; Floris van Doorn (RTA-TLCA, 2014)

The Lean Theorem Prover (System Description). - Leonardo Mendonça de Moura; Soonho Kong; Jeremy Avigad; Floris van Doorn; Jakob von Raumer (CADE, 2015)

Propositional Calculus in Coq. - Floris van Doorn (CoRR, 2015)

Constructing the propositional truncation using non-recursive HITs. - Floris van Doorn (CPP, 2016)

Homotopy Type Theory in Lean. - Floris van Doorn; Jakob von Raumer; Ulrik Buchholtz (ITP, 2017)

Higher Groups in Homotopy Type Theory. - Ulrik Buchholtz; Floris van Doorn; Egbert Rijke (LICS, 2018)

On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. - Floris van Doorn (CoRR, 2018)

A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. - Jesse Michael Han; Floris van Doorn (ITP, 2019)

A formal proof of the independence of the continuum hypothesis. - Jesse Michael Han; Floris van Doorn (CPP, 2020)

Sequential Colimits in Homotopy Type Theory. - Kristina Sojakova; Floris van Doorn; Egbert Rijke (LICS, 2020)

Maintaining a Library of Formal Mathematics. - Floris van Doorn; Gabriel Ebner; Robert Y. Lewis (CICM, 2020)

Progress on a perimeter surveillance problem. - Jeremy Avigad; Floris van Doorn (CoRR, 2020)

Formalized Haar Measure. - Floris van Doorn (ITP, 2021)

Designing a general library for convolutions. - Floris van Doorn (CoRR, 2022)

Formalising the h-Principle and Sphere Eversion. - Floris van Doorn; Patrick Massot; Oliver Nash (CPP, 2023)

Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. - Floris van Doorn; Heather Macbeth (ITP, 2024)