- Higher Inductive Types, talk at FSCD/UF 2016, Porto.
- Programming with Higher Inductive Types, talk at EUTYPES meeting, Ljubljana.
- The Three-HITs Theorem, talk at FPFM workshop, Nantes.
- Higher Inductive Types in Programming, talk at Agda Implementors Meeting XXV, Gothenburg.
- Finite Sets in HoTT, talk at EUTYPES meeting in Nijmegen
- 1-Types vs Groupoids, talk at TYPES2018, Braga
- Bicategories in Homotopy Type Theory, talk at EUTYPES meeting in Aarhus
- Category Theory in UniMath, talk at UniMath School II 2019, Birmingham
- Bicategories in Univalent Foundations, talk at TYPES2019, Oslo
- Bicategories in Univalent Foundations, talk at FSCD2019, Dortmund
- Constructing 1-truncated finitary higher inductive types as groupoid quotients, talk at HoTTEST2020
- Constructing Higher Inductive Types as Groupoid Quotients, talk at LICS2020
- Semantics for two-dimensional type theory, talk at Syntax and Semantics of Type Theories, Stockholm
- Semantics for two-dimensional type theory, talk at TYPES2022, Nantes

- Henning Basold, Herman Geuvers, Niels van der Weide

Programming with Higher Inductive Types, Journal of Universal Computer Science, Vol. 23, No. 1, pp. 63-88. - Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide

Finite Sets in Homotopy Type Theory, CPP, pp. 201--214, ACM 2018.

Webpage - Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide

Bicategories in Univalent Foundations, FSCD 2019, Vol. 131, pp. 5:1-5:17. - Niccolò Veltri and Niels van der Weide

Guarded Recursion in Agda via Sized Types, FSCD 2019, Vol. 131, pp. 31:1-32:19.

Repository - Niels van der Weide and Herman Geuvers

The Construction of Set-Truncated Higher Inductive Types, MFPS 2019, Vol.237 of ENTC, pp. 261-280

Repository - Niels van der Weide

Constructing Higher Inductive Types as Groupoid Quotients, LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, July 2020, Pages 929–943. - Niccolò Veltri and Niels van der Weide

Constructing Higher Inductive Types as Groupoid Quotients, Logical Methods in Computer Science, Volume 17, Issue 2, 2021, pp. 8:1–8:42. - Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide

Bicategories in Univalent Foundations, Mathematical Structures in Computer Science, 1-38. - Benedikt Ahrens, Paige Randall North, Niels van der Weide

Semantics for two-dimensional type theory, LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, August 2022, Article 12, 1-14.

- Dan Frumin, Herman Geuvers, Niels van der Weide

1-Types vs Groupoids, TYPES2018, Braga - Henning Basold, Niccolò Veltri, Niels van der Weide

Free Algebraic Theories as Higher Inductive Types, TYPES2019, Oslo - Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide

Bicategories in Univalent Foundations, TYPES2019, Oslo - Niccolò Veltri, Niels van der Weide

Guarded Recursion in Agda via Sized Types, TYPES2019, Oslo - Niels van der Weide

Constructing Higher Inductive Types as Groupoid Quotients, TYPES2020 - Deivid Vale, Niels van der Weide

Formalizing Higher-Order Termination in Coq, WST2021 - Benedikt Ahrens, Paige Randall North, Niels van der Weide

Semantics for two-dimensional type theory, TYPES2022, Nantes - Benedikt Ahrens, Paige Randall North, Niels van der Weide

Semantics for two-dimensional type theory, HoTT/UF2022, Haifa

- Computing Exact Solutions of Initial Value Problems, Bachelor Thesis Computer Science
- Model Structures on Toposes, Master Thesis Mathematics
- Higher Inductive Types, Master Thesis Computer Science
- Constructing Higher Inductive Types, PhD Thesis Computer Science