- 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 2020, pp. 929–943. - Benedikt Ahrens, Paige Randall North, Niels van der Weide

Semantics for two-dimensional type theory, LICS 2022, pp. 1-14. - Niels van der Weide

The Formal Theory of Monads, Univalently, FSCD 2023, Vol. 260, pp. 6:1-6:23. - Niels van der Weide, Deivid Vale, Cynthia Kop

Certifying Higher-Order Polynomial Interpretations, ITP 2023, Vol. 268, pp. 30:1-30:20.

- 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. - 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, Submitted.

- Higher Inductive Types, talk at HoTT/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.
- The Construction of Set-Truncated Higher Inductive Types, talk at MFPS. London.
- 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.
- Category Theory in UniMath, talk at UniMath School III 2022, Cortona, Italy.
- Enriched Categories in Univalent Foundations, talk at HoTT/UF 2023, Vienna, Austria.
- Enriched Categories in Univalent Foundations, talk at TYPES 2023, Valencia, Spain.
- The Formal Theory of Monads, Univalently, talk at FSCD 2023, Rome, Italy.

- 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 - Niels van der Weide

Enriched Categories in Univalent Foundations, HoTT/UF2023, Vienna - Niels van der Weide

Enriched Categories in Univalent Foundations, Types 2023, Valencia

- 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