### Papers and preprints

- Higher Groups in Homotopy Type Theory, with Floris van Doorn and Egbert Rijke: arXiv
- Cellular Cohomology in Homotopy Type Theory, with Kuen-Bang Hou (Favonia): arXiv
- Syntactic Forcing Models for Coherent Logic, with Marc Bezem and Thierry Coquand: arXiv
- Homotopy Type Theory in Lean, with Floris van Doorn and Jakob von Raumer: arXiv, doi
- The real projective spaces in homotopy type theory, with Egbert Rijke: arXiv, doi
- Varieties of Cubical Sets, with Edward Morehouse: arXiv, doi
- The Cayley-Dickson Construction in Homotopy Type Theory, with Egbert Rijke: preprint, arXiv
- Theories of proof-theoretic strength ψ(Γ
_{Ω+1}), with Gerhard Jäger and Thomas Strahm: preprint, doi

### Topics

- Formal systems for Foundations of Mathematics
- Homotopy Type Theory
- Feferman's Unfolding Program & Explicit Mathematics

### Talks

Various expository and research talks I've given:

- From Higher Groups to Homotopy Surfaces, HoTTEST, March 29, 2018: video, slides
- Formalizing type theory in type theory using nominal techniques, HoTT/UF Workshop, FSCD 2017, Oxford, UK, September 9, 2017: slides
- Nominal applications of the classifying space of the finitary permutation group, Big Proof meeting at the Isaac Newton Institute, Cambridge, UK, July 6, 2017: abstract and video
- Higher groups and projective spaces in HoTT, CMU, September 23, 2016: notes
- Proof theory of homotopy type theory: what we know so far, FoMUS talk, July 22, 2016: slides
- Synthetic homotopy theory and higher inductive types, FoMUS workshop, July, 2016: slides
- The quaternionic Hopf fibration in HoTT, CMU, January 22, 2016: video (cf. slides prepared for a similar talk at MPIM in Bonn, February 12, 2016; however, I used the blackboards instead.)
- Primitive recursive homotopy type theory, ASL meeting in Urbana, March 28, 2015.
- Proof-theoretic ordinals related to unfoldings, Münchenwiler, October, 2014: slides
- Lower bounds in type theory with ordinals and universes, Münchenwiler, June 20, 2014: slides
- Survey of systems of strength ψ(Γ
_{Ω+1}), PCC 2014, Paris: slides - Two operational systems of strength ψ(Γ
_{Ω+1}), March 13, 2014: slides - The Unfolding of Systems of Inductive Definitions, October 31, 2013: slides
- Univalent Foundations and the Structure Identity Principle, January 8, 2013: slides
- Formalizing forcing arguments in subsystems of second-order arithmetic, April 26, 2011: slides
- Functional interpretation and inductive definitions, February 1, 2011: slides
- Transfinitely iterated fixpoint theories, October 26 and November 2, 2010: slides
- Functional interpretation of arithmetical comprehension, May 27, 2010: slides
- Normalization of intuitionistic set theories, April 13, 2010: slides
- Geometric theorem proving, March 3, 2010: slides
- Girard-Reynolds System F, December 3, 2009: slides

### PhD Thesis

December 6, 2013 I finished my PhD thesis at Stanford University under the direction of Solomon Feferman. You can download my thesis here: Unfolding of Systems of Inductive Definitions. If you want a paper version, it can be acquired cheaply from amazon.com, amazon.co.uk, amazon.de, and other book sellers.

### MSc Thesis

I wrote my MSc thesis at the University of Copenhagen. My advisor was Jesper Grodal, and you can download my thesis here: The Atiyah-Segal Completion Theorem.